Recent Additions to the Intuitionistic Logic
Explorer
Date | Label | Description |
Theorem |
|
17-Mar-2023 | finct 6848 |
A finite set is countable. (Contributed by Jim Kingdon,
17-Mar-2023.)
|
 
     ⊔    |
|
16-Mar-2023 | ctmlemr 6844 |
Lemma for ctm 6845. One of the directions of the biconditional.
(Contributed by Jim Kingdon, 16-Mar-2023.)
|
   
   
      ⊔     |
|
15-Mar-2023 | caseinl 6836 |
Applying the "case" construction to a left injection. (Contributed
by
Jim Kingdon, 15-Mar-2023.)
|
       case     inl  
      |
|
13-Mar-2023 | enumct 6847 |
A finitely enumerable set is countable. Lemma 8.1.14 of [AczelRathjen],
p. 73 (except that our definition of countable does not require the set
to be inhabited). "Finitely enumerable" is defined as
       
per Definition 8.1.4 of
[AczelRathjen], p. 71 and
"countable" is defined as
       ⊔ 
per [BauerSwan], p. 14:3.
(Contributed by Jim Kingdon, 13-Mar-2023.)
|
      
      ⊔    |
|
13-Mar-2023 | enumctlemm 6846 |
Lemma for enumct 6847. The case where is greater than zero.
(Contributed by Jim Kingdon, 13-Mar-2023.)
|
         
                      |
|
13-Mar-2023 | ctm 6845 |
Two equivalent definitions of countable for an inhabited set. Remark of
[BauerSwan], p. 14:3. (Contributed by
Jim Kingdon, 13-Mar-2023.)
|
   
     ⊔          |
|
13-Mar-2023 | 0ct 6843 |
The empty set is countable. Remark of [BauerSwan], p. 14:3 which also
has the definition of countable used here. (Contributed by Jim Kingdon,
13-Mar-2023.)
|
      ⊔   |
|
13-Mar-2023 | ctex 6524 |
A class dominated by is a set. (Contributed by Thierry Arnoux,
29-Dec-2016.) (Proof shortened by Jim Kingdon, 13-Mar-2023.)
|
   |
|
12-Mar-2023 | cls0 11894 |
The closure of the empty set. (Contributed by NM, 2-Oct-2007.) (Proof
shortened by Jim Kingdon, 12-Mar-2023.)
|
           |
|
12-Mar-2023 | algrp1 11367 |
The value of the algorithm iterator at   .
(Contributed by Paul Chapman, 31-Mar-2011.) (Revised by Jim Kingdon,
12-Mar-2023.)
|
                               
            |
|
12-Mar-2023 | ialgr0 11365 |
The value of the algorithm iterator at is the
initial state
. (Contributed
by Paul Chapman, 31-Mar-2011.) (Revised by Jim
Kingdon, 12-Mar-2023.)
|
                                |
|
11-Mar-2023 | ntreq0 11893 |
Two ways to say that a subset has an empty interior. (Contributed by
NM, 3-Oct-2007.) (Revised by Jim Kingdon, 11-Mar-2023.)
|
  
         
 
    |
|
11-Mar-2023 | clstop 11888 |
The closure of a topology's underlying set is the entire set.
(Contributed by NM, 5-Oct-2007.) (Proof shortened by Jim Kingdon,
11-Mar-2023.)
|
 
          |
|
11-Mar-2023 | ntrss 11880 |
Subset relationship for interior. (Contributed by NM, 3-Oct-2007.)
(Revised by Jim Kingdon, 11-Mar-2023.)
|
  
                   |
|
10-Mar-2023 | iuncld 11876 |
A finite indexed union of closed sets is closed. (Contributed by Mario
Carneiro, 19-Sep-2015.) (Revised by Jim Kingdon, 10-Mar-2023.)
|
        
       |
|
5-Mar-2023 | 2basgeng 11843 |
Conditions that determine the equality of two generated topologies.
(Contributed by NM, 8-May-2007.) (Revised by Jim Kingdon,
5-Mar-2023.)
|
 
               |
|
5-Mar-2023 | exmidsssn 4040 |
Excluded middle is equivalent to the biconditionalized version of
sssnr 3603 for sets. (Contributed by Jim Kingdon,
5-Mar-2023.)
|
EXMID     
         |
|
5-Mar-2023 | exmidn0m 4039 |
Excluded middle is equivalent to any set being empty or inhabited.
(Contributed by Jim Kingdon, 5-Mar-2023.)
|
EXMID        |
|
4-Mar-2023 | eltg3 11818 |
Membership in a topology generated by a basis. (Contributed by NM,
15-Jul-2006.) (Revised by Jim Kingdon, 4-Mar-2023.)
|
              |
|
4-Mar-2023 | tgvalex 11811 |
The topology generated by a basis is a set. (Contributed by Jim
Kingdon, 4-Mar-2023.)
|
       |
|
16-Feb-2023 | ixp0 6502 |
The infinite Cartesian product of a family    with an empty
member is empty. (Contributed by NM, 1-Oct-2006.) (Revised by Jim
Kingdon, 16-Feb-2023.)
|
     |
|
16-Feb-2023 | ixpm 6501 |
If an infinite Cartesian product of a family    is inhabited,
every    is inhabited. (Contributed by Mario Carneiro,
22-Jun-2016.) (Revised by Jim Kingdon, 16-Feb-2023.)
|
    
  |
|
16-Feb-2023 | exmidundifim 4044 |
Excluded middle is equivalent to every subset having a complement.
Variation of exmidundif 4043 with an implication rather than a
biconditional. (Contributed by Jim Kingdon, 16-Feb-2023.)
|
EXMID     
       |
|
15-Feb-2023 | ixpintm 6496 |
The intersection of a collection of infinite Cartesian products.
(Contributed by Mario Carneiro, 3-Feb-2015.) (Revised by Jim Kingdon,
15-Feb-2023.)
|
        |
|
15-Feb-2023 | ixpiinm 6495 |
The indexed intersection of a collection of infinite Cartesian products.
(Contributed by Mario Carneiro, 6-Feb-2015.) (Revised by Jim Kingdon,
15-Feb-2023.)
|
   
    |
|
15-Feb-2023 | ixpexgg 6493 |
The existence of an infinite Cartesian product. is normally a
free-variable parameter in . Remark in Enderton p. 54.
(Contributed by NM, 28-Sep-2006.) (Revised by Jim Kingdon,
15-Feb-2023.)
|
    
  |
|
15-Feb-2023 | nfixpxy 6488 |
Bound-variable hypothesis builder for indexed Cartesian product.
(Contributed by Mario Carneiro, 15-Oct-2016.) (Revised by Jim Kingdon,
15-Feb-2023.)
|
        |
|
13-Feb-2023 | topnpropgd 11727 |
The topology extractor function depends only on the base and topology
components. (Contributed by NM, 18-Jul-2006.) (Revised by Jim Kingdon,
13-Feb-2023.)
|
           TopSet  TopSet                  |
|
12-Feb-2023 | slotex 11582 |
Existence of slot value. A corollary of slotslfn 11581. (Contributed by
Jim Kingdon, 12-Feb-2023.)
|
 Slot              
  |
|
11-Feb-2023 | topnvalg 11725 |
Value of the topology extractor function. (Contributed by Mario
Carneiro, 13-Aug-2015.) (Revised by Jim Kingdon, 11-Feb-2023.)
|
    TopSet   
↾t        |
|
10-Feb-2023 | slotslfn 11581 |
A slot is a function on sets, treated as structures. (Contributed by
Mario Carneiro, 22-Sep-2015.) (Revised by Jim Kingdon, 10-Feb-2023.)
|
 Slot           |
|
9-Feb-2023 | pleslid 11712 |
Slot property of .
(Contributed by Jim Kingdon, 9-Feb-2023.)
|
 Slot           |
|
9-Feb-2023 | topgrptsetd 11709 |
The topology of a constructed topological group. (Contributed by Mario
Carneiro, 29-Aug-2015.) (Revised by Jim Kingdon, 9-Feb-2023.)
|
                TopSet       
    TopSet    |
|
9-Feb-2023 | topgrpplusgd 11708 |
The additive operation of a constructed topological group. (Contributed
by Mario Carneiro, 29-Aug-2015.) (Revised by Jim Kingdon,
9-Feb-2023.)
|
                TopSet       
         |
|
9-Feb-2023 | topgrpbasd 11707 |
The base set of a constructed topological group. (Contributed by Mario
Carneiro, 29-Aug-2015.) (Revised by Jim Kingdon, 9-Feb-2023.)
|
                TopSet       
          |
|
9-Feb-2023 | topgrpstrd 11706 |
A constructed topological group is a structure. (Contributed by Mario
Carneiro, 29-Aug-2015.) (Revised by Jim Kingdon, 9-Feb-2023.)
|
                TopSet       
    Struct      |
|
9-Feb-2023 | tsetslid 11705 |
Slot property of TopSet. (Contributed by Jim Kingdon,
9-Feb-2023.)
|
TopSet Slot
TopSet  TopSet 
  |
|
8-Feb-2023 | ipsipd 11702 |
The multiplicative operation of a constructed inner product space.
(Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Jim Kingdon,
8-Feb-2023.)
|
                         Scalar                       
     
          |
|
8-Feb-2023 | ipsvscad 11701 |
The scalar product operation of a constructed inner product space.
(Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Jim Kingdon,
8-Feb-2023.)
|
                         Scalar                       
     
          |
|
8-Feb-2023 | ipsscad 11700 |
The set of scalars of a constructed inner product space. (Contributed
by Stefan O'Rear, 27-Nov-2014.) (Revised by Jim Kingdon,
8-Feb-2023.)
|
                         Scalar                       
     
    Scalar    |
|
7-Feb-2023 | ipsmulrd 11699 |
The multiplicative operation of a constructed inner product space.
(Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Jim Kingdon,
7-Feb-2023.)
|
                         Scalar                       
     
          |
|
7-Feb-2023 | ipsaddgd 11698 |
The additive operation of a constructed inner product space.
(Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Jim Kingdon,
7-Feb-2023.)
|
                         Scalar                       
     
         |
|
7-Feb-2023 | ipsbased 11697 |
The base set of a constructed inner product space. (Contributed by
Stefan O'Rear, 27-Nov-2014.) (Revised by Jim Kingdon, 7-Feb-2023.)
|
                         Scalar                       
     
          |
|
7-Feb-2023 | ipsstrd 11696 |
A constructed inner product space is a structure. (Contributed by
Stefan O'Rear, 27-Nov-2014.) (Revised by Jim Kingdon, 7-Feb-2023.)
|
                         Scalar                       
     
    Struct      |
|
7-Feb-2023 | ipslid 11695 |
Slot property of .
(Contributed by Jim Kingdon, 7-Feb-2023.)
|
 Slot           |
|
7-Feb-2023 | lmodvscad 11692 |
The scalar product operation of a constructed left vector space.
(Contributed by Mario Carneiro, 2-Oct-2013.) (Revised by Jim Kingdon,
7-Feb-2023.)
|
                 Scalar           
        
        |
|
6-Feb-2023 | lmodscad 11691 |
The set of scalars of a constructed left vector space. (Contributed by
Mario Carneiro, 2-Oct-2013.) (Revised by Jim Kingdon, 6-Feb-2023.)
|
                 Scalar           
        
  Scalar    |
|
6-Feb-2023 | lmodplusgd 11690 |
The additive operation of a constructed left vector space. (Contributed
by Mario Carneiro, 2-Oct-2013.) (Revised by Jim Kingdon,
6-Feb-2023.)
|
                 Scalar           
        
       |
|
6-Feb-2023 | lmodbased 11689 |
The base set of a constructed left vector space. (Contributed by Mario
Carneiro, 2-Oct-2013.) (Revised by Jim Kingdon, 6-Feb-2023.)
|
                 Scalar           
        
        |
|
5-Feb-2023 | lmodstrd 11688 |
A constructed left module or left vector space is a structure.
(Contributed by Mario Carneiro, 1-Oct-2013.) (Revised by Jim Kingdon,
5-Feb-2023.)
|
                 Scalar           
        
  Struct      |
|
5-Feb-2023 | vscaslid 11687 |
Slot property of .
(Contributed by Jim Kingdon, 5-Feb-2023.)
|
 Slot           |
|
5-Feb-2023 | scaslid 11684 |
Slot property of Scalar. (Contributed by Jim Kingdon,
5-Feb-2023.)
|
Scalar Slot
Scalar  Scalar 
  |
|
5-Feb-2023 | srngplusgd 11679 |
The addition operation of a constructed star ring. (Contributed by
Mario Carneiro, 20-Jun-2015.) (Revised by Jim Kingdon, 5-Feb-2023.)
|
                                   
           |
|
5-Feb-2023 | srngbased 11678 |
The base set of a constructed star ring. (Contributed by Mario
Carneiro, 18-Nov-2013.) (Revised by Jim Kingdon, 5-Feb-2023.)
|
                                   
            |
|
5-Feb-2023 | srngstrd 11677 |
A constructed star ring is a structure. (Contributed by Mario Carneiro,
18-Nov-2013.) (Revised by Jim Kingdon, 5-Feb-2023.)
|
                                   
      Struct      |
|
5-Feb-2023 | opelstrsl 11651 |
The slot of a structure which contains an ordered pair for that slot.
(Contributed by Jim Kingdon, 5-Feb-2023.)
|
 Slot           Struct                    |
|
4-Feb-2023 | starvslid 11676 |
Slot property of  . (Contributed by Jim
Kingdon, 4-Feb-2023.)
|
  Slot     
       |
|
3-Feb-2023 | rngbaseg 11671 |
The base set of a constructed ring. (Contributed by Mario Carneiro,
2-Oct-2013.) (Revised by Jim Kingdon, 3-Feb-2023.)
|
                        
      |
|
3-Feb-2023 | rngstrg 11670 |
A constructed ring is a structure. (Contributed by Mario Carneiro,
28-Sep-2013.) (Revised by Jim Kingdon, 3-Feb-2023.)
|
                        
Struct      |
|
3-Feb-2023 | mulrslid 11667 |
Slot property of .
(Contributed by Jim Kingdon, 3-Feb-2023.)
|
 Slot           |
|
3-Feb-2023 | plusgslid 11650 |
Slot property of . (Contributed by Jim Kingdon, 3-Feb-2023.)
|
 Slot         |
|
2-Feb-2023 | 2strop1g 11660 |
The other slot of a constructed two-slot structure. Version of
2stropg 11657 not depending on the hard-coded index value
of the base set.
(Contributed by AV, 22-Sep-2020.) (Revised by Jim Kingdon,
2-Feb-2023.)
|
                Slot  

      |
|
2-Feb-2023 | 2strbas1g 11659 |
The base set of a constructed two-slot structure. Version of 2strbasg 11656
not depending on the hard-coded index value of the base set.
(Contributed by AV, 22-Sep-2020.) (Revised by Jim Kingdon,
2-Feb-2023.)
|
                         |
|
2-Feb-2023 | 2strstr1g 11658 |
A constructed two-slot structure. Version of 2strstrg 11655 not depending
on the hard-coded index value of the base set. (Contributed by AV,
22-Sep-2020.) (Revised by Jim Kingdon, 2-Feb-2023.)
|
                   Struct      
   |
|
31-Jan-2023 | baseslid 11611 |
The base set extractor is a slot. (Contributed by Jim Kingdon,
31-Jan-2023.)
|

Slot           |
|
31-Jan-2023 | strsl0 11603 |
All components of the empty set are empty sets. (Contributed by Stefan
O'Rear, 27-Nov-2014.) (Revised by Jim Kingdon, 31-Jan-2023.)
|
 Slot               |
|
31-Jan-2023 | strslss 11602 |
Propagate component extraction to a structure from a subset
structure .
(Contributed by Mario Carneiro, 11-Oct-2013.)
(Revised by Jim Kingdon, 31-Jan-2023.)
|
 Slot        
           
     |
|
31-Jan-2023 | strslssd 11601 |
Deduction version of strslss 11602. (Contributed by Mario Carneiro,
15-Nov-2014.) (Revised by Mario Carneiro, 30-Apr-2015.) (Revised by
Jim Kingdon, 31-Jan-2023.)
|
 Slot            
                       |
|
30-Jan-2023 | strslfv3 11600 |
Variant on strslfv 11599 for large structures. (Contributed by Mario
Carneiro, 10-Jan-2017.) (Revised by Jim Kingdon, 30-Jan-2023.)
|
  Struct
 Slot        
                   |
|
30-Jan-2023 | strslfv 11599 |
Extract a structure component (such as the base set) from a
structure with
a component extractor
(such as the base set
extractor df-base 11561). By virtue of ndxslid 11580, this can be done
without having to refer to the hard-coded numeric index of .
(Contributed by Mario Carneiro, 6-Oct-2013.) (Revised by Jim Kingdon,
30-Jan-2023.)
|
Struct  Slot        
          
      |
|
30-Jan-2023 | strslfv2 11598 |
A variation on strslfv 11599 to avoid asserting that itself is a
function, which involves sethood of all the ordered pair components of
. (Contributed
by Mario Carneiro, 30-Apr-2015.) (Revised by Jim
Kingdon, 30-Jan-2023.)
|
   Slot        
               |
|
30-Jan-2023 | strslfv2d 11597 |
Deduction version of strslfv 11599. (Contributed by Mario Carneiro,
30-Apr-2015.) (Revised by Jim Kingdon, 30-Jan-2023.)
|
 Slot            
         
           |
|
30-Jan-2023 | strslfvd 11596 |
Deduction version of strslfv 11599. (Contributed by Mario Carneiro,
15-Nov-2014.) (Revised by Jim Kingdon, 30-Jan-2023.)
|
 Slot            
                 |
|
30-Jan-2023 | strsetsid 11588 |
Value of the structure replacement function. (Contributed by AV,
14-Mar-2020.) (Revised by Jim Kingdon, 30-Jan-2023.)
|
Slot      Struct     
 
       sSet               |
|
30-Jan-2023 | funresdfunsndc 6279 |
Restricting a function to a domain without one element of the domain of
the function, and adding a pair of this element and the function value
of the element results in the function itself, where equality is
decidable. (Contributed by AV, 2-Dec-2018.) (Revised by Jim Kingdon,
30-Jan-2023.)
|
     DECID
                    |
|
29-Jan-2023 | ndxslid 11580 |
A structure component extractor is defined by its own index. That the
index is a natural number will also be needed in quite a few contexts so
it is included in the conclusion of this theorem which can be used as a
hypothesis of theorems like strslfv 11599. (Contributed by Jim Kingdon,
29-Jan-2023.)
|
Slot  Slot           |
|
29-Jan-2023 | fnsnsplitdc 6278 |
Split a function into a single point and all the rest. (Contributed by
Stefan O'Rear, 27-Feb-2015.) (Revised by Jim Kingdon, 29-Jan-2023.)
|
    DECID                     |
|
28-Jan-2023 | 2stropg 11657 |
The other slot of a constructed two-slot structure. (Contributed by
Mario Carneiro, 29-Aug-2015.) (Revised by Jim Kingdon, 28-Jan-2023.)
|
                Slot          |
|
28-Jan-2023 | 2strbasg 11656 |
The base set of a constructed two-slot structure. (Contributed by Mario
Carneiro, 29-Aug-2015.) (Revised by Jim Kingdon, 28-Jan-2023.)
|
                Slot          |
|
28-Jan-2023 | 2strstrg 11655 |
A constructed two-slot structure. (Contributed by Mario Carneiro,
29-Aug-2015.) (Revised by Jim Kingdon, 28-Jan-2023.)
|
                Slot    Struct      |
|
28-Jan-2023 | 1strstrg 11653 |
A constructed one-slot structure. (Contributed by AV, 27-Mar-2020.)
(Revised by Jim Kingdon, 28-Jan-2023.)
|
          Struct      |
|
27-Jan-2023 | strle2g 11646 |
Make a structure from a pair. (Contributed by Mario Carneiro,
29-Aug-2015.) (Revised by Jim Kingdon, 27-Jan-2023.)
|
            Struct      |
|
27-Jan-2023 | strle1g 11645 |
Make a structure from a singleton. (Contributed by Mario Carneiro,
29-Aug-2015.) (Revised by Jim Kingdon, 27-Jan-2023.)
|
      Struct      |
|
27-Jan-2023 | strleund 11643 |
Combine two structures into one. (Contributed by Mario Carneiro,
29-Aug-2015.) (Revised by Jim Kingdon, 27-Jan-2023.)
|
 Struct  
  
Struct          Struct      |
|
26-Jan-2023 | ressid2 11614 |
General behavior of trivial restriction. (Contributed by Stefan O'Rear,
29-Nov-2014.) (Revised by Jim Kingdon, 26-Jan-2023.)
|
 ↾s        
  |
|
24-Jan-2023 | setsslnid 11606 |
Value of the structure replacement function at an untouched index.
(Contributed by Mario Carneiro, 1-Dec-2014.) (Revised by Jim Kingdon,
24-Jan-2023.)
|
 Slot             
      
    sSet        |
|
24-Jan-2023 | setsslid 11605 |
Value of the structure replacement function at a replaced index.
(Contributed by Mario Carneiro, 1-Dec-2014.) (Revised by Jim Kingdon,
24-Jan-2023.)
|
 Slot                 sSet      
     |
|
22-Jan-2023 | setsabsd 11594 |
Replacing the same components twice yields the same as the second
setting only. (Contributed by Mario Carneiro, 2-Dec-2014.) (Revised by
Jim Kingdon, 22-Jan-2023.)
|
           sSet
    sSet
     sSet       |
|
22-Jan-2023 | setsresg 11593 |
The structure replacement function does not affect the value of away
from .
(Contributed by Mario Carneiro, 1-Dec-2014.) (Revised by
Jim Kingdon, 22-Jan-2023.)
|
     sSet                  |
|
22-Jan-2023 | setsex 11587 |
Applying the structure replacement function yields a set. (Contributed by
Jim Kingdon, 22-Jan-2023.)
|
    sSet       |
|
22-Jan-2023 | 2zsupmax 10718 |
Two ways to express the maximum of two integers. Because order of
integers is decidable, we have more flexibility than for real numbers.
(Contributed by Jim Kingdon, 22-Jan-2023.)
|
           
 
   |
|
22-Jan-2023 | elpwpwel 4310 |
A class belongs to a double power class if and only if its union belongs
to the power class. (Contributed by BJ, 22-Jan-2023.)
|
  
    |
|
21-Jan-2023 | funresdfunsnss 5514 |
Restricting a function to a domain without one element of the domain of
the function, and adding a pair of this element and the function value of
the element results in a subset of the function itself. (Contributed by
AV, 2-Dec-2018.) (Revised by Jim Kingdon, 21-Jan-2023.)
|
                   
  |
|
20-Jan-2023 | setsvala 11586 |
Value of the structure replacement function. (Contributed by Mario
Carneiro, 1-Dec-2014.) (Revised by Jim Kingdon, 20-Jan-2023.)
|
    sSet                    |
|
20-Jan-2023 | fnsnsplitss 5510 |
Split a function into a single point and all the rest. (Contributed by
Stefan O'Rear, 27-Feb-2015.) (Revised by Jim Kingdon, 20-Jan-2023.)
|
                   
  |
|
19-Jan-2023 | strfvssn 11577 |
A structure component extractor produces a value which is contained in a
set dependent on , but not .
This is sometimes useful for
showing sethood. (Contributed by Mario Carneiro, 15-Aug-2015.)
(Revised by Jim Kingdon, 19-Jan-2023.)
|
Slot             |
|
19-Jan-2023 | strnfvn 11576 |
Value of a structure component extractor . Normally, is a
defined constant symbol such as (df-base 11561) and is a
fixed integer such as . is a
structure, i.e. a specific
member of a class of structures.
Note: Normally, this theorem shouldn't be used outside of this section,
because it requires hard-coded index values. Instead, use strslfv 11599.
(Contributed by NM, 9-Sep-2011.) (Revised by Jim Kingdon, 19-Jan-2023.)
(New usage is discouraged.)
|
Slot          |
|
19-Jan-2023 | strnfvnd 11575 |
Deduction version of strnfvn 11576. (Contributed by Mario Carneiro,
15-Nov-2014.) (Revised by Jim Kingdon, 19-Jan-2023.)
|
Slot                |
|
18-Jan-2023 | isstructr 11570 |
The property of being a structure with components in   .
(Contributed by Mario Carneiro, 29-Aug-2015.) (Revised by Jim Kingdon,
18-Jan-2023.)
|
               Struct      |
|
18-Jan-2023 | isstructim 11569 |
The property of being a structure with components in   .
(Contributed by Mario Carneiro, 29-Aug-2015.) (Revised by Jim Kingdon,
18-Jan-2023.)
|
 Struct
                 |