:: COMBGRAS  semantic presentation begin  











theorem :: COMBGRAS:1 (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set (Var "b"))) & (Bool (Set   ($#k1_card_1 :::"card"::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set (Var "n"))) & (Bool (Set   ($#k1_card_1 :::"card"::: )  (Set (Var "b")))  ($#r1_hidden :::"="::: )  (Set (Var "n")))) "holds"  (Bool  "("  (Bool (Set   ($#k1_card_1 :::"card"::: )  (Set  "(" (Set (Var "a"))  ($#k3_xboole_0 :::"/\"::: )  (Set (Var "b")) ")" ))  ($#r2_hidden :::"in"::: )  (Set (Var "n"))) & (Bool (Set (Set (Var "n"))  ($#k2_nat_1 :::"+"::: )  (Num 1))  ($#r1_ordinal1 :::"c="::: )  (Set   ($#k1_card_1 :::"card"::: )  (Set  "(" (Set (Var "a"))  ($#k2_xboole_0 :::"\/"::: )  (Set (Var "b")) ")" )))  ")" ))) ; 
 
theorem :: COMBGRAS:2 (Bool  "for" (Set (Var "n")) "," (Set (Var "k")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set   ($#k1_card_1 :::"card"::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "n"))  ($#k2_nat_1 :::"+"::: )  (Set (Var "k")))) & (Bool (Set   ($#k1_card_1 :::"card"::: )  (Set (Var "b")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "n"))  ($#k2_nat_1 :::"+"::: )  (Set (Var "k"))))) "holds"  (Bool  "("  (Bool (Set   ($#k1_card_1 :::"card"::: )  (Set  "(" (Set (Var "a"))  ($#k3_xboole_0 :::"/\"::: )  (Set (Var "b")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "n"))) "iff" (Bool (Set   ($#k1_card_1 :::"card"::: )  (Set  "(" (Set (Var "a"))  ($#k2_xboole_0 :::"\/"::: )  (Set (Var "b")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "n"))  ($#k2_nat_1 :::"+"::: )  (Set  "(" (Num 2)  ($#k4_nat_1 :::"*"::: )  (Set (Var "k")) ")" )))  ")" ))) ; 
 
theorem :: COMBGRAS:3 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set   ($#k1_card_1 :::"card"::: )  (Set (Var "X")))  ($#r1_ordinal1 :::"c="::: )  (Set   ($#k1_card_1 :::"card"::: )  (Set (Var "Y")))) "iff" (Bool  "ex" (Set (Var "f")) "being"   ($#m1_hidden :::"Function":::) "st"  (Bool  "("  (Bool (Set (Var "f")) "is"   ($#v2_funct_1 :::"one-to-one"::: )  ) & (Bool (Set (Var "X"))  ($#r1_tarski :::"c="::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "f")))) & (Bool (Set (Set (Var "f"))  ($#k7_relat_1 :::".:"::: )  (Set (Var "X")))  ($#r1_tarski :::"c="::: )  (Set (Var "Y")))  ")" ))  ")" )) ; 
 
theorem :: COMBGRAS:4 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "f")) "being"   ($#m1_hidden :::"Function":::)  "st" (Bool (Bool (Set (Var "f")) "is"   ($#v2_funct_1 :::"one-to-one"::: )  ) & (Bool (Set (Var "X"))  ($#r1_tarski :::"c="::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "f"))))) "holds"  (Bool (Set   ($#k1_card_1 :::"card"::: )  (Set  "(" (Set (Var "f"))  ($#k7_relat_1 :::".:"::: )  (Set (Var "X")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k1_card_1 :::"card"::: )  (Set (Var "X")))))) ; 
 
theorem :: COMBGRAS:5 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Set (Var "X"))  ($#k6_subset_1 :::"\"::: )  (Set (Var "Y")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "X"))  ($#k6_subset_1 :::"\"::: )  (Set (Var "Z")))) & (Bool (Set (Var "Y"))  ($#r1_tarski :::"c="::: )  (Set (Var "X"))) & (Bool (Set (Var "Z"))  ($#r1_tarski :::"c="::: )  (Set (Var "X")))) "holds"  (Bool (Set (Var "Y"))  ($#r1_hidden :::"="::: )  (Set (Var "Z")))) ; 
 
theorem :: COMBGRAS:6 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "Y")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y"))  "st" (Bool (Bool (Set (Var "p")) "is"   ($#v2_funct_1 :::"one-to-one"::: )  )) "holds"  (Bool  "for" (Set (Var "x1")) "," (Set (Var "x2")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X"))  "st" (Bool (Bool (Set (Var "x1"))  ($#r1_hidden :::"<>"::: )  (Set (Var "x2")))) "holds"  (Bool (Set (Set (Var "p"))  ($#k7_relat_1 :::".:"::: )  (Set (Var "x1")))  ($#r1_hidden :::"<>"::: )  (Set (Set (Var "p"))  ($#k7_relat_1 :::".:"::: )  (Set (Var "x2")))))))) ; 
 
theorem :: COMBGRAS:7 (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set   ($#k1_card_1 :::"card"::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "n"))  ($#k5_real_1 :::"-"::: )  (Num 1))) & (Bool (Set   ($#k1_card_1 :::"card"::: )  (Set (Var "b")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "n"))  ($#k5_real_1 :::"-"::: )  (Num 1))) & (Bool (Set   ($#k1_card_1 :::"card"::: )  (Set (Var "c")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "n"))  ($#k5_real_1 :::"-"::: )  (Num 1))) & (Bool (Set   ($#k1_card_1 :::"card"::: )  (Set  "(" (Set (Var "a"))  ($#k3_xboole_0 :::"/\"::: )  (Set (Var "b")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "n"))  ($#k5_real_1 :::"-"::: )  (Num 2))) & (Bool (Set   ($#k1_card_1 :::"card"::: )  (Set  "(" (Set (Var "a"))  ($#k3_xboole_0 :::"/\"::: )  (Set (Var "c")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "n"))  ($#k5_real_1 :::"-"::: )  (Num 2))) & (Bool (Set   ($#k1_card_1 :::"card"::: )  (Set  "(" (Set (Var "b"))  ($#k3_xboole_0 :::"/\"::: )  (Set (Var "c")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "n"))  ($#k5_real_1 :::"-"::: )  (Num 2))) & (Bool (Num 2)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "n")))) "holds"  (Bool  "("  (Bool  "("   "not" (Bool (Num 3)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "n"))) "or" (Bool  "("  (Bool (Set   ($#k1_card_1 :::"card"::: )  (Set  "(" (Set  "(" (Set (Var "a"))  ($#k3_xboole_0 :::"/\"::: )  (Set (Var "b")) ")" )  ($#k3_xboole_0 :::"/\"::: )  (Set (Var "c")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "n"))  ($#k5_real_1 :::"-"::: )  (Num 2))) & (Bool (Set   ($#k1_card_1 :::"card"::: )  (Set  "(" (Set  "(" (Set (Var "a"))  ($#k2_xboole_0 :::"\/"::: )  (Set (Var "b")) ")" )  ($#k2_xboole_0 :::"\/"::: )  (Set (Var "c")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "n"))  ($#k2_nat_1 :::"+"::: )  (Num 1)))  ")" ) "or" (Bool  "("  (Bool (Set   ($#k1_card_1 :::"card"::: )  (Set  "(" (Set  "(" (Set (Var "a"))  ($#k3_xboole_0 :::"/\"::: )  (Set (Var "b")) ")" )  ($#k3_xboole_0 :::"/\"::: )  (Set (Var "c")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "n"))  ($#k5_real_1 :::"-"::: )  (Num 3))) & (Bool (Set   ($#k1_card_1 :::"card"::: )  (Set  "(" (Set  "(" (Set (Var "a"))  ($#k2_xboole_0 :::"\/"::: )  (Set (Var "b")) ")" )  ($#k2_xboole_0 :::"\/"::: )  (Set (Var "c")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "n")))  ")" )  ")" ) &  "("  (Bool (Bool (Set (Var "n"))  ($#r1_hidden :::"="::: )  (Num 2))) "implies" (Bool  "("  (Bool (Set   ($#k1_card_1 :::"card"::: )  (Set  "(" (Set  "(" (Set (Var "a"))  ($#k3_xboole_0 :::"/\"::: )  (Set (Var "b")) ")" )  ($#k3_xboole_0 :::"/\"::: )  (Set (Var "c")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "n"))  ($#k5_real_1 :::"-"::: )  (Num 2))) & (Bool (Set   ($#k1_card_1 :::"card"::: )  (Set  "(" (Set  "(" (Set (Var "a"))  ($#k2_xboole_0 :::"\/"::: )  (Set (Var "b")) ")" )  ($#k2_xboole_0 :::"\/"::: )  (Set (Var "c")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "n"))  ($#k2_nat_1 :::"+"::: )  (Num 1)))  ")" )  ")"   ")" ))) ; 
 
theorem :: COMBGRAS:8 (Bool  "for" (Set (Var "P1")) "," (Set (Var "P2")) "being"    ($#l1_incsp_1 :::"IncProjStr"::: )    "st" (Bool (Bool (Set   ($#g1_incsp_1 :::"IncProjStr"::: )  "(#"  (Set  "the"  ($#u1_incsp_1 :::"Points"::: )  "of" (Set (Var "P1"))) "," (Set  "the"  ($#u2_incsp_1 :::"Lines"::: )  "of" (Set (Var "P1"))) "," (Set  "the"  ($#u3_incsp_1 :::"Inc"::: )  "of" (Set (Var "P1"))) "#)" )  ($#r1_hidden :::"="::: )  (Set   ($#g1_incsp_1 :::"IncProjStr"::: )  "(#"  (Set  "the"  ($#u1_incsp_1 :::"Points"::: )  "of" (Set (Var "P2"))) "," (Set  "the"  ($#u2_incsp_1 :::"Lines"::: )  "of" (Set (Var "P2"))) "," (Set  "the"  ($#u3_incsp_1 :::"Inc"::: )  "of" (Set (Var "P2"))) "#)" ))) "holds"  (Bool  "for" (Set (Var "A1")) "being"   ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "P1"))  (Bool  "for" (Set (Var "A2")) "being"   ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "P2"))  "st" (Bool (Bool (Set (Var "A1"))  ($#r1_hidden :::"="::: )  (Set (Var "A2")))) "holds"  (Bool  "for" (Set (Var "L1")) "being"   ($#m1_subset_1 :::"LINE":::) "of" (Set (Var "P1"))  (Bool  "for" (Set (Var "L2")) "being"   ($#m1_subset_1 :::"LINE":::) "of" (Set (Var "P2"))  "st" (Bool (Bool (Set (Var "L1"))  ($#r1_hidden :::"="::: )  (Set (Var "L2"))) & (Bool (Set (Var "A1"))  ($#r1_incsp_1 :::"on"::: )  (Set (Var "L1")))) "holds"  (Bool (Set (Var "A2"))  ($#r1_incsp_1 :::"on"::: )  (Set (Var "L2")))))))) ; 
 
theorem :: COMBGRAS:9 (Bool  "for" (Set (Var "P1")) "," (Set (Var "P2")) "being"    ($#l1_incsp_1 :::"IncProjStr"::: )    "st" (Bool (Bool (Set   ($#g1_incsp_1 :::"IncProjStr"::: )  "(#"  (Set  "the"  ($#u1_incsp_1 :::"Points"::: )  "of" (Set (Var "P1"))) "," (Set  "the"  ($#u2_incsp_1 :::"Lines"::: )  "of" (Set (Var "P1"))) "," (Set  "the"  ($#u3_incsp_1 :::"Inc"::: )  "of" (Set (Var "P1"))) "#)" )  ($#r1_hidden :::"="::: )  (Set   ($#g1_incsp_1 :::"IncProjStr"::: )  "(#"  (Set  "the"  ($#u1_incsp_1 :::"Points"::: )  "of" (Set (Var "P2"))) "," (Set  "the"  ($#u2_incsp_1 :::"Lines"::: )  "of" (Set (Var "P2"))) "," (Set  "the"  ($#u3_incsp_1 :::"Inc"::: )  "of" (Set (Var "P2"))) "#)" ))) "holds"  (Bool  "for" (Set (Var "A1")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "the"  ($#u1_incsp_1 :::"Points"::: )  "of" (Set (Var "P1")))  (Bool  "for" (Set (Var "A2")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "the"  ($#u1_incsp_1 :::"Points"::: )  "of" (Set (Var "P2")))  "st" (Bool (Bool (Set (Var "A1"))  ($#r1_hidden :::"="::: )  (Set (Var "A2")))) "holds"  (Bool  "for" (Set (Var "L1")) "being"   ($#m1_subset_1 :::"LINE":::) "of" (Set (Var "P1"))  (Bool  "for" (Set (Var "L2")) "being"   ($#m1_subset_1 :::"LINE":::) "of" (Set (Var "P2"))  "st" (Bool (Bool (Set (Var "L1"))  ($#r1_hidden :::"="::: )  (Set (Var "L2"))) & (Bool (Set (Var "A1"))  ($#r4_incsp_1 :::"on"::: )  (Set (Var "L1")))) "holds"  (Bool (Set (Var "A2"))  ($#r4_incsp_1 :::"on"::: )  (Set (Var "L2")))))))) ; 
 registration
cluster   ($#v1_incsp_1 :::"strict"::: )     ($#v5_incsp_1 :::"with_non-trivial_lines"::: )     ($#v6_incsp_1 :::"linear"::: )     ($#v7_incsp_1 :::"up-2-rank"::: )    for    ($#l1_incsp_1 :::"IncProjStr"::: )  ; 
end; begin  definitionmode PartialLinearSpace is   ($#v5_incsp_1 :::"with_non-trivial_lines"::: )     ($#v7_incsp_1 :::"up-2-rank"::: )     ($#l1_incsp_1 :::"IncProjStr"::: )  ; end; definitionlet "k" be    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ); let "X" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  ; assume that  
(Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set (Const "k")))
 and  
(Bool (Set (Set (Const "k"))  ($#k2_nat_1 :::"+"::: )  (Num 1))  ($#r1_ordinal1 :::"c="::: )  (Set   ($#k1_card_1 :::"card"::: )  (Set (Const "X"))))
 ; func  :::"G_":::  "(" "k" "," "X" ")"  ->   ($#v1_incsp_1 :::"strict"::: )    ($#l1_incsp_1 :::"PartialLinearSpace":::) means :: COMBGRAS:def 1 (Bool  "("  (Bool (Set  "the"  ($#u1_incsp_1 :::"Points"::: )  "of" it)  ($#r1_hidden :::"="::: )   "{"  (Set (Var "A")) where A "is"   ($#m1_subset_1 :::"Subset":::) "of" "X" : (Bool (Set   ($#k1_card_1 :::"card"::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  "k")  "}"  ) & (Bool (Set  "the"  ($#u2_incsp_1 :::"Lines"::: )  "of" it)  ($#r1_hidden :::"="::: )   "{"  (Set (Var "L")) where L "is"   ($#m1_subset_1 :::"Subset":::) "of" "X" : (Bool (Set   ($#k1_card_1 :::"card"::: )  (Set (Var "L")))  ($#r1_hidden :::"="::: )  (Set "k"  ($#k2_nat_1 :::"+"::: )  (Num 1)))  "}"  ) & (Bool (Set  "the"  ($#u3_incsp_1 :::"Inc"::: )  "of" it)  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k1_wellord2 :::"RelIncl"::: )  (Set  "("  ($#k9_setfam_1 :::"bool"::: )  "X" ")" ) ")" )  ($#k3_xboole_0 :::"/\"::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  "the"  ($#u1_incsp_1 :::"Points"::: )  "of" it) "," (Set  "the"  ($#u2_incsp_1 :::"Lines"::: )  "of" it) ($#k2_zfmisc_1 :::":]"::: ) )))  ")" ); end; 







:: deftheorem    defines :::"G_"::: COMBGRAS:def 1 :  (Bool  "for" (Set (Var "k")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "X")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "k"))) & (Bool (Set (Set (Var "k"))  ($#k2_nat_1 :::"+"::: )  (Num 1))  ($#r1_ordinal1 :::"c="::: )  (Set   ($#k1_card_1 :::"card"::: )  (Set (Var "X"))))) "holds"  (Bool  "for" (Set (Var "b3")) "being"   ($#v1_incsp_1 :::"strict"::: )    ($#l1_incsp_1 :::"PartialLinearSpace":::) "holds"   (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_combgras :::"G_"::: )   "(" (Set (Var "k")) "," (Set (Var "X")) ")" )) "iff" (Bool  "("  (Bool (Set  "the"  ($#u1_incsp_1 :::"Points"::: )  "of" (Set (Var "b3")))  ($#r1_hidden :::"="::: )   "{"  (Set (Var "A")) where A "is"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) : (Bool (Set   ($#k1_card_1 :::"card"::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set (Var "k")))  "}"  ) & (Bool (Set  "the"  ($#u2_incsp_1 :::"Lines"::: )  "of" (Set (Var "b3")))  ($#r1_hidden :::"="::: )   "{"  (Set (Var "L")) where L "is"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) : (Bool (Set   ($#k1_card_1 :::"card"::: )  (Set (Var "L")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "k"))  ($#k2_nat_1 :::"+"::: )  (Num 1)))  "}"  ) & (Bool (Set  "the"  ($#u3_incsp_1 :::"Inc"::: )  "of" (Set (Var "b3")))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k1_wellord2 :::"RelIncl"::: )  (Set  "("  ($#k9_setfam_1 :::"bool"::: )  (Set (Var "X")) ")" ) ")" )  ($#k3_xboole_0 :::"/\"::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  "the"  ($#u1_incsp_1 :::"Points"::: )  "of" (Set (Var "b3"))) "," (Set  "the"  ($#u2_incsp_1 :::"Lines"::: )  "of" (Set (Var "b3"))) ($#k2_zfmisc_1 :::":]"::: ) )))  ")" )  ")" )))); 
 
theorem :: COMBGRAS:10 (Bool  "for" (Set (Var "k")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "X")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "k"))) & (Bool (Set (Set (Var "k"))  ($#k2_nat_1 :::"+"::: )  (Num 1))  ($#r1_ordinal1 :::"c="::: )  (Set   ($#k1_card_1 :::"card"::: )  (Set (Var "X"))))) "holds"  (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"POINT":::) "of" (Set  "("  ($#k1_combgras :::"G_"::: )   "(" (Set (Var "k")) "," (Set (Var "X")) ")"  ")" )  (Bool  "for" (Set (Var "L")) "being"   ($#m1_subset_1 :::"LINE":::) "of" (Set  "("  ($#k1_combgras :::"G_"::: )   "(" (Set (Var "k")) "," (Set (Var "X")) ")"  ")" ) "holds"   (Bool  "("  (Bool (Set (Var "A"))  ($#r1_incsp_1 :::"on"::: )  (Set (Var "L"))) "iff" (Bool (Set (Var "A"))  ($#r1_tarski :::"c="::: )  (Set (Var "L")))  ")" ))))) ; 
 
theorem :: COMBGRAS:11 (Bool  "for" (Set (Var "k")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "X")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "k"))) & (Bool (Set (Set (Var "k"))  ($#k2_nat_1 :::"+"::: )  (Num 1))  ($#r1_ordinal1 :::"c="::: )  (Set   ($#k1_card_1 :::"card"::: )  (Set (Var "X"))))) "holds"  (Bool (Set   ($#k1_combgras :::"G_"::: )   "(" (Set (Var "k")) "," (Set (Var "X")) ")" ) "is"   ($#v4_incproj :::"Vebleian"::: )  ))) ; 
 
theorem :: COMBGRAS:12 (Bool  "for" (Set (Var "k")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "X")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "k"))) & (Bool (Set (Set (Var "k"))  ($#k2_nat_1 :::"+"::: )  (Num 1))  ($#r1_ordinal1 :::"c="::: )  (Set   ($#k1_card_1 :::"card"::: )  (Set (Var "X"))))) "holds"  (Bool  "for" (Set (Var "A1")) "," (Set (Var "A2")) "," (Set (Var "A3")) "," (Set (Var "A4")) "," (Set (Var "A5")) "," (Set (Var "A6")) "being"   ($#m1_subset_1 :::"POINT":::) "of" (Set  "("  ($#k1_combgras :::"G_"::: )   "(" (Set (Var "k")) "," (Set (Var "X")) ")"  ")" )  (Bool  "for" (Set (Var "L1")) "," (Set (Var "L2")) "," (Set (Var "L3")) "," (Set (Var "L4")) "being"   ($#m1_subset_1 :::"LINE":::) "of" (Set  "("  ($#k1_combgras :::"G_"::: )   "(" (Set (Var "k")) "," (Set (Var "X")) ")"  ")" )  "st" (Bool (Bool (Set (Var "A1"))  ($#r1_incsp_1 :::"on"::: )  (Set (Var "L1"))) & (Bool (Set (Var "A2"))  ($#r1_incsp_1 :::"on"::: )  (Set (Var "L1"))) & (Bool (Set (Var "A3"))  ($#r1_incsp_1 :::"on"::: )  (Set (Var "L2"))) & (Bool (Set (Var "A4"))  ($#r1_incsp_1 :::"on"::: )  (Set (Var "L2"))) & (Bool (Set (Var "A5"))  ($#r1_incsp_1 :::"on"::: )  (Set (Var "L1"))) & (Bool (Set (Var "A5"))  ($#r1_incsp_1 :::"on"::: )  (Set (Var "L2"))) & (Bool (Set (Var "A1"))  ($#r1_incsp_1 :::"on"::: )  (Set (Var "L3"))) & (Bool (Set (Var "A3"))  ($#r1_incsp_1 :::"on"::: )  (Set (Var "L3"))) & (Bool (Set (Var "A2"))  ($#r1_incsp_1 :::"on"::: )  (Set (Var "L4"))) & (Bool (Set (Var "A4"))  ($#r1_incsp_1 :::"on"::: )  (Set (Var "L4"))) & (Bool (Bool  "not" (Set (Var "A5"))  ($#r1_incsp_1 :::"on"::: )  (Set (Var "L3")))) & (Bool (Bool  "not" (Set (Var "A5"))  ($#r1_incsp_1 :::"on"::: )  (Set (Var "L4")))) & (Bool (Set (Var "L1"))  ($#r1_hidden :::"<>"::: )  (Set (Var "L2"))) & (Bool (Set (Var "L3"))  ($#r1_hidden :::"<>"::: )  (Set (Var "L4")))) "holds"  (Bool  "ex" (Set (Var "A6")) "being"   ($#m1_subset_1 :::"POINT":::) "of" (Set  "("  ($#k1_combgras :::"G_"::: )   "(" (Set (Var "k")) "," (Set (Var "X")) ")"  ")" ) "st"  (Bool  "("  (Bool (Set (Var "A6"))  ($#r1_incsp_1 :::"on"::: )  (Set (Var "L3"))) & (Bool (Set (Var "A6"))  ($#r1_incsp_1 :::"on"::: )  (Set (Var "L4"))) & (Bool (Set (Var "A6"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "A1"))  ($#k3_xboole_0 :::"/\"::: )  (Set (Var "A2")) ")" )  ($#k2_xboole_0 :::"\/"::: )  (Set  "(" (Set (Var "A3"))  ($#k3_xboole_0 :::"/\"::: )  (Set (Var "A4")) ")" )))  ")" )))))) ; 
 
theorem :: COMBGRAS:13 (Bool  "for" (Set (Var "k")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "X")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "k"))) & (Bool (Set (Set (Var "k"))  ($#k2_nat_1 :::"+"::: )  (Num 1))  ($#r1_ordinal1 :::"c="::: )  (Set   ($#k1_card_1 :::"card"::: )  (Set (Var "X"))))) "holds"  (Bool (Set   ($#k1_combgras :::"G_"::: )   "(" (Set (Var "k")) "," (Set (Var "X")) ")" ) "is"   ($#v9_incproj :::"Desarguesian"::: )  ))) ; 
 definitionlet "S" be    ($#l1_incsp_1 :::"IncProjStr"::: )  ; let "K" be   ($#m1_subset_1 :::"Subset":::) "of" (Set  "the"  ($#u1_incsp_1 :::"Points"::: )  "of" (Set (Const "S"))); attr "K" is  :::"clique":::  means :: COMBGRAS:def 2 (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#m1_subset_1 :::"POINT":::) "of" "S"  "st" (Bool (Bool (Set (Var "A"))  ($#r2_hidden :::"in"::: )  "K") & (Bool (Set (Var "B"))  ($#r2_hidden :::"in"::: )  "K")) "holds"  (Bool  "ex" (Set (Var "L")) "being"   ($#m1_subset_1 :::"LINE":::) "of" "S" "st" (Bool (Set  ($#k7_domain_1 :::"{"::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k7_domain_1 :::"}"::: ) )  ($#r4_incsp_1 :::"on"::: )  (Set (Var "L"))))); end; 





:: deftheorem    defines :::"clique"::: COMBGRAS:def 2 :  (Bool  "for" (Set (Var "S")) "being"    ($#l1_incsp_1 :::"IncProjStr"::: )    (Bool  "for" (Set (Var "K")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "the"  ($#u1_incsp_1 :::"Points"::: )  "of" (Set (Var "S"))) "holds"   (Bool  "("  (Bool (Set (Var "K")) "is"   ($#v1_combgras :::"clique"::: )  ) "iff" (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "S"))  "st" (Bool (Bool (Set (Var "A"))  ($#r2_hidden :::"in"::: )  (Set (Var "K"))) & (Bool (Set (Var "B"))  ($#r2_hidden :::"in"::: )  (Set (Var "K")))) "holds"  (Bool  "ex" (Set (Var "L")) "being"   ($#m1_subset_1 :::"LINE":::) "of" (Set (Var "S")) "st" (Bool (Set  ($#k7_domain_1 :::"{"::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k7_domain_1 :::"}"::: ) )  ($#r4_incsp_1 :::"on"::: )  (Set (Var "L")))))  ")" ))); 
 definitionlet "S" be    ($#l1_incsp_1 :::"IncProjStr"::: )  ; let "K" be   ($#m1_subset_1 :::"Subset":::) "of" (Set  "the"  ($#u1_incsp_1 :::"Points"::: )  "of" (Set (Const "S"))); attr "K" is  :::"maximal_clique":::  means :: COMBGRAS:def 3 (Bool  "("  (Bool "K" "is"   ($#v1_combgras :::"clique"::: )  ) & (Bool  "("   "for" (Set (Var "U")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "the"  ($#u1_incsp_1 :::"Points"::: )  "of" "S")  "st" (Bool (Bool (Set (Var "U")) "is"   ($#v1_combgras :::"clique"::: )  ) & (Bool "K"  ($#r1_tarski :::"c="::: )  (Set (Var "U")))) "holds"  (Bool (Set (Var "U"))  ($#r1_hidden :::"="::: )  "K")  ")" )  ")" ); end; 





:: deftheorem    defines :::"maximal_clique"::: COMBGRAS:def 3 :  (Bool  "for" (Set (Var "S")) "being"    ($#l1_incsp_1 :::"IncProjStr"::: )    (Bool  "for" (Set (Var "K")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "the"  ($#u1_incsp_1 :::"Points"::: )  "of" (Set (Var "S"))) "holds"   (Bool  "("  (Bool (Set (Var "K")) "is"   ($#v2_combgras :::"maximal_clique"::: )  ) "iff" (Bool  "("  (Bool (Set (Var "K")) "is"   ($#v1_combgras :::"clique"::: )  ) & (Bool  "("   "for" (Set (Var "U")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "the"  ($#u1_incsp_1 :::"Points"::: )  "of" (Set (Var "S")))  "st" (Bool (Bool (Set (Var "U")) "is"   ($#v1_combgras :::"clique"::: )  ) & (Bool (Set (Var "K"))  ($#r1_tarski :::"c="::: )  (Set (Var "U")))) "holds"  (Bool (Set (Var "U"))  ($#r1_hidden :::"="::: )  (Set (Var "K")))  ")" )  ")" )  ")" ))); 
 definitionlet "k" be    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ); let "X" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  ; let "T" be   ($#m1_subset_1 :::"Subset":::) "of" (Set  "the"  ($#u1_incsp_1 :::"Points"::: )  "of" (Set  "("  ($#k1_combgras :::"G_"::: )   "(" (Set (Const "k")) "," (Set (Const "X")) ")"  ")" )); attr "T" is  :::"STAR":::  means :: COMBGRAS:def 4 (Bool  "ex" (Set (Var "S")) "being"   ($#m1_subset_1 :::"Subset":::) "of" "X" "st"  (Bool  "("  (Bool (Set   ($#k1_card_1 :::"card"::: )  (Set (Var "S")))  ($#r1_hidden :::"="::: )  (Set "k"  ($#k5_real_1 :::"-"::: )  (Num 1))) & (Bool "T"  ($#r1_hidden :::"="::: )   "{"  (Set (Var "A")) where A "is"   ($#m1_subset_1 :::"Subset":::) "of" "X" : (Bool  "("  (Bool (Set   ($#k1_card_1 :::"card"::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  "k") & (Bool (Set (Var "S"))  ($#r1_tarski :::"c="::: )  (Set (Var "A")))  ")" )  "}"  )  ")" )); attr "T" is  :::"TOP":::  means :: COMBGRAS:def 5 (Bool  "ex" (Set (Var "S")) "being"   ($#m1_subset_1 :::"Subset":::) "of" "X" "st"  (Bool  "("  (Bool (Set   ($#k1_card_1 :::"card"::: )  (Set (Var "S")))  ($#r1_hidden :::"="::: )  (Set "k"  ($#k2_nat_1 :::"+"::: )  (Num 1))) & (Bool "T"  ($#r1_hidden :::"="::: )   "{"  (Set (Var "A")) where A "is"   ($#m1_subset_1 :::"Subset":::) "of" "X" : (Bool  "("  (Bool (Set   ($#k1_card_1 :::"card"::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  "k") & (Bool (Set (Var "A"))  ($#r1_tarski :::"c="::: )  (Set (Var "S")))  ")" )  "}"  )  ")" )); end; 












:: deftheorem    defines :::"STAR"::: COMBGRAS:def 4 :  (Bool  "for" (Set (Var "k")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "X")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "T")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "the"  ($#u1_incsp_1 :::"Points"::: )  "of" (Set  "("  ($#k1_combgras :::"G_"::: )   "(" (Set (Var "k")) "," (Set (Var "X")) ")"  ")" )) "holds"   (Bool  "("  (Bool (Set (Var "T")) "is"   ($#v3_combgras :::"STAR"::: )  ) "iff" (Bool  "ex" (Set (Var "S")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st"  (Bool  "("  (Bool (Set   ($#k1_card_1 :::"card"::: )  (Set (Var "S")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "k"))  ($#k5_real_1 :::"-"::: )  (Num 1))) & (Bool (Set (Var "T"))  ($#r1_hidden :::"="::: )   "{"  (Set (Var "A")) where A "is"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) : (Bool  "("  (Bool (Set   ($#k1_card_1 :::"card"::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set (Var "k"))) & (Bool (Set (Var "S"))  ($#r1_tarski :::"c="::: )  (Set (Var "A")))  ")" )  "}"  )  ")" ))  ")" )))); 
 
:: deftheorem    defines :::"TOP"::: COMBGRAS:def 5 :  (Bool  "for" (Set (Var "k")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "X")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "T")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "the"  ($#u1_incsp_1 :::"Points"::: )  "of" (Set  "("  ($#k1_combgras :::"G_"::: )   "(" (Set (Var "k")) "," (Set (Var "X")) ")"  ")" )) "holds"   (Bool  "("  (Bool (Set (Var "T")) "is"   ($#v4_combgras :::"TOP"::: )  ) "iff" (Bool  "ex" (Set (Var "S")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st"  (Bool  "("  (Bool (Set   ($#k1_card_1 :::"card"::: )  (Set (Var "S")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "k"))  ($#k2_nat_1 :::"+"::: )  (Num 1))) & (Bool (Set (Var "T"))  ($#r1_hidden :::"="::: )   "{"  (Set (Var "A")) where A "is"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) : (Bool  "("  (Bool (Set   ($#k1_card_1 :::"card"::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set (Var "k"))) & (Bool (Set (Var "A"))  ($#r1_tarski :::"c="::: )  (Set (Var "S")))  ")" )  "}"  )  ")" ))  ")" )))); 
 
theorem :: COMBGRAS:14 (Bool  "for" (Set (Var "k")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "X")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Num 2)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "k"))) & (Bool (Set (Set (Var "k"))  ($#k2_nat_1 :::"+"::: )  (Num 2))  ($#r1_ordinal1 :::"c="::: )  (Set   ($#k1_card_1 :::"card"::: )  (Set (Var "X"))))) "holds"  (Bool  "for" (Set (Var "K")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "the"  ($#u1_incsp_1 :::"Points"::: )  "of" (Set  "("  ($#k1_combgras :::"G_"::: )   "(" (Set (Var "k")) "," (Set (Var "X")) ")"  ")" ))  "st" (Bool (Bool  "("  (Bool (Set (Var "K")) "is"   ($#v3_combgras :::"STAR"::: )  ) "or" (Bool (Set (Var "K")) "is"   ($#v4_combgras :::"TOP"::: )  )  ")" )) "holds"  (Bool (Set (Var "K")) "is"   ($#v2_combgras :::"maximal_clique"::: )  )))) ; 
 
theorem :: COMBGRAS:15 (Bool  "for" (Set (Var "k")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "X")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Num 2)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "k"))) & (Bool (Set (Set (Var "k"))  ($#k2_nat_1 :::"+"::: )  (Num 2))  ($#r1_ordinal1 :::"c="::: )  (Set   ($#k1_card_1 :::"card"::: )  (Set (Var "X"))))) "holds"  (Bool  "for" (Set (Var "K")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "the"  ($#u1_incsp_1 :::"Points"::: )  "of" (Set  "("  ($#k1_combgras :::"G_"::: )   "(" (Set (Var "k")) "," (Set (Var "X")) ")"  ")" ))  "holds"  (Bool  "("   "not" (Bool (Set (Var "K")) "is"   ($#v2_combgras :::"maximal_clique"::: )  ) "or" (Bool (Set (Var "K")) "is"   ($#v3_combgras :::"STAR"::: )  ) "or" (Bool (Set (Var "K")) "is"   ($#v4_combgras :::"TOP"::: )  )  ")" )))) ; 
 begin  definitionlet "S1", "S2" be    ($#l1_incsp_1 :::"IncProjStr"::: )  ; attr "c3" is  :::"strict"::: ; struct  :::"IncProjMap":::  "over" "S1" "," "S2" -> ; aggr :::"IncProjMap":::(# :::"point-map":::, :::"line-map"::: #) ->    ($#l1_combgras :::"IncProjMap"::: )   "over" "S1" "," "S2"; sel  :::"point-map"::: "c3" ->   ($#m1_subset_1 :::"Function":::) "of" (Set  "the"  ($#u1_incsp_1 :::"Points"::: )  "of" "S1") "," (Set  "the"  ($#u1_incsp_1 :::"Points"::: )  "of" "S2"); sel  :::"line-map"::: "c3" ->   ($#m1_subset_1 :::"Function":::) "of" (Set  "the"  ($#u2_incsp_1 :::"Lines"::: )  "of" "S1") "," (Set  "the"  ($#u2_incsp_1 :::"Lines"::: )  "of" "S2"); end; definitionlet "S1", "S2" be    ($#l1_incsp_1 :::"IncProjStr"::: )  ; let "F" be    ($#l1_combgras :::"IncProjMap"::: )   "over" (Set (Const "S1")) "," (Set (Const "S2")); let "a" be   ($#m1_subset_1 :::"POINT":::) "of" (Set (Const "S1")); func "F" :::"."::: "a" ->   ($#m1_subset_1 :::"POINT":::) "of" "S2" equals :: COMBGRAS:def 6 (Set (Set  "the"  ($#u1_combgras :::"point-map"::: )  "of" "F")  ($#k3_funct_2 :::"."::: )  "a"); end; 








:: deftheorem    defines :::"."::: COMBGRAS:def 6 :  (Bool  "for" (Set (Var "S1")) "," (Set (Var "S2")) "being"    ($#l1_incsp_1 :::"IncProjStr"::: )    (Bool  "for" (Set (Var "F")) "being"    ($#l1_combgras :::"IncProjMap"::: )   "over" (Set (Var "S1")) "," (Set (Var "S2"))  (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "S1")) "holds"  (Bool (Set (Set (Var "F"))  ($#k2_combgras :::"."::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set (Set  "the"  ($#u1_combgras :::"point-map"::: )  "of" (Set (Var "F")))  ($#k3_funct_2 :::"."::: )  (Set (Var "a"))))))); 
 definitionlet "S1", "S2" be    ($#l1_incsp_1 :::"IncProjStr"::: )  ; let "F" be    ($#l1_combgras :::"IncProjMap"::: )   "over" (Set (Const "S1")) "," (Set (Const "S2")); let "L" be   ($#m1_subset_1 :::"LINE":::) "of" (Set (Const "S1")); func "F" :::"."::: "L" ->   ($#m1_subset_1 :::"LINE":::) "of" "S2" equals :: COMBGRAS:def 7 (Set (Set  "the"  ($#u2_combgras :::"line-map"::: )  "of" "F")  ($#k3_funct_2 :::"."::: )  "L"); end; 








:: deftheorem    defines :::"."::: COMBGRAS:def 7 :  (Bool  "for" (Set (Var "S1")) "," (Set (Var "S2")) "being"    ($#l1_incsp_1 :::"IncProjStr"::: )    (Bool  "for" (Set (Var "F")) "being"    ($#l1_combgras :::"IncProjMap"::: )   "over" (Set (Var "S1")) "," (Set (Var "S2"))  (Bool  "for" (Set (Var "L")) "being"   ($#m1_subset_1 :::"LINE":::) "of" (Set (Var "S1")) "holds"  (Bool (Set (Set (Var "F"))  ($#k3_combgras :::"."::: )  (Set (Var "L")))  ($#r1_hidden :::"="::: )  (Set (Set  "the"  ($#u2_combgras :::"line-map"::: )  "of" (Set (Var "F")))  ($#k3_funct_2 :::"."::: )  (Set (Var "L"))))))); 
 
theorem :: COMBGRAS:16 (Bool  "for" (Set (Var "S1")) "," (Set (Var "S2")) "being"    ($#l1_incsp_1 :::"IncProjStr"::: )    (Bool  "for" (Set (Var "F1")) "," (Set (Var "F2")) "being"    ($#l1_combgras :::"IncProjMap"::: )   "over" (Set (Var "S1")) "," (Set (Var "S2"))  "st" (Bool (Bool  "("   "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "S1")) "holds"  (Bool (Set (Set (Var "F1"))  ($#k2_combgras :::"."::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "F2"))  ($#k2_combgras :::"."::: )  (Set (Var "A"))))  ")" ) & (Bool  "("   "for" (Set (Var "L")) "being"   ($#m1_subset_1 :::"LINE":::) "of" (Set (Var "S1")) "holds"  (Bool (Set (Set (Var "F1"))  ($#k3_combgras :::"."::: )  (Set (Var "L")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "F2"))  ($#k3_combgras :::"."::: )  (Set (Var "L"))))  ")" )) "holds"  (Bool (Set   ($#g1_combgras :::"IncProjMap"::: )  "(#"  (Set  "the"  ($#u1_combgras :::"point-map"::: )  "of" (Set (Var "F1"))) "," (Set  "the"  ($#u2_combgras :::"line-map"::: )  "of" (Set (Var "F1"))) "#)" )  ($#r1_hidden :::"="::: )  (Set   ($#g1_combgras :::"IncProjMap"::: )  "(#"  (Set  "the"  ($#u1_combgras :::"point-map"::: )  "of" (Set (Var "F2"))) "," (Set  "the"  ($#u2_combgras :::"line-map"::: )  "of" (Set (Var "F2"))) "#)" )))) ; 
 definitionlet "S1", "S2" be    ($#l1_incsp_1 :::"IncProjStr"::: )  ; let "F" be    ($#l1_combgras :::"IncProjMap"::: )   "over" (Set (Const "S1")) "," (Set (Const "S2")); attr "F" is  :::"incidence_preserving":::  means :: COMBGRAS:def 8 (Bool  "for" (Set (Var "A1")) "being"   ($#m1_subset_1 :::"POINT":::) "of" "S1"  (Bool  "for" (Set (Var "L1")) "being"   ($#m1_subset_1 :::"LINE":::) "of" "S1" "holds"   (Bool  "("  (Bool (Set (Var "A1"))  ($#r1_incsp_1 :::"on"::: )  (Set (Var "L1"))) "iff" (Bool (Set "F"  ($#k2_combgras :::"."::: )  (Set (Var "A1")))  ($#r1_incsp_1 :::"on"::: )  (Set "F"  ($#k3_combgras :::"."::: )  (Set (Var "L1"))))  ")" ))); end; 






:: deftheorem    defines :::"incidence_preserving"::: COMBGRAS:def 8 :  (Bool  "for" (Set (Var "S1")) "," (Set (Var "S2")) "being"    ($#l1_incsp_1 :::"IncProjStr"::: )    (Bool  "for" (Set (Var "F")) "being"    ($#l1_combgras :::"IncProjMap"::: )   "over" (Set (Var "S1")) "," (Set (Var "S2")) "holds"   (Bool  "("  (Bool (Set (Var "F")) "is"   ($#v6_combgras :::"incidence_preserving"::: )  ) "iff" (Bool  "for" (Set (Var "A1")) "being"   ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "S1"))  (Bool  "for" (Set (Var "L1")) "being"   ($#m1_subset_1 :::"LINE":::) "of" (Set (Var "S1")) "holds"   (Bool  "("  (Bool (Set (Var "A1"))  ($#r1_incsp_1 :::"on"::: )  (Set (Var "L1"))) "iff" (Bool (Set (Set (Var "F"))  ($#k2_combgras :::"."::: )  (Set (Var "A1")))  ($#r1_incsp_1 :::"on"::: )  (Set (Set (Var "F"))  ($#k3_combgras :::"."::: )  (Set (Var "L1"))))  ")" )))  ")" ))); 
 
theorem :: COMBGRAS:17 (Bool  "for" (Set (Var "S1")) "," (Set (Var "S2")) "being"    ($#l1_incsp_1 :::"IncProjStr"::: )    (Bool  "for" (Set (Var "F1")) "," (Set (Var "F2")) "being"    ($#l1_combgras :::"IncProjMap"::: )   "over" (Set (Var "S1")) "," (Set (Var "S2"))  "st" (Bool (Bool (Set   ($#g1_combgras :::"IncProjMap"::: )  "(#"  (Set  "the"  ($#u1_combgras :::"point-map"::: )  "of" (Set (Var "F1"))) "," (Set  "the"  ($#u2_combgras :::"line-map"::: )  "of" (Set (Var "F1"))) "#)" )  ($#r1_hidden :::"="::: )  (Set   ($#g1_combgras :::"IncProjMap"::: )  "(#"  (Set  "the"  ($#u1_combgras :::"point-map"::: )  "of" (Set (Var "F2"))) "," (Set  "the"  ($#u2_combgras :::"line-map"::: )  "of" (Set (Var "F2"))) "#)" )) & (Bool (Set (Var "F1")) "is"   ($#v6_combgras :::"incidence_preserving"::: )  )) "holds"  (Bool (Set (Var "F2")) "is"   ($#v6_combgras :::"incidence_preserving"::: )  ))) ; 
 definitionlet "S" be    ($#l1_incsp_1 :::"IncProjStr"::: )  ; let "F" be    ($#l1_combgras :::"IncProjMap"::: )   "over" (Set (Const "S")) "," (Set (Const "S")); attr "F" is  :::"automorphism":::  means :: COMBGRAS:def 9 (Bool  "("  (Bool (Set  "the"  ($#u2_combgras :::"line-map"::: )  "of" "F") "is"   ($#v3_funct_2 :::"bijective"::: )  ) & (Bool (Set  "the"  ($#u1_combgras :::"point-map"::: )  "of" "F") "is"   ($#v3_funct_2 :::"bijective"::: )  ) & (Bool "F" "is"   ($#v6_combgras :::"incidence_preserving"::: )  )  ")" ); end; 





:: deftheorem    defines :::"automorphism"::: COMBGRAS:def 9 :  (Bool  "for" (Set (Var "S")) "being"    ($#l1_incsp_1 :::"IncProjStr"::: )    (Bool  "for" (Set (Var "F")) "being"    ($#l1_combgras :::"IncProjMap"::: )   "over" (Set (Var "S")) "," (Set (Var "S")) "holds"   (Bool  "("  (Bool (Set (Var "F")) "is"   ($#v7_combgras :::"automorphism"::: )  ) "iff" (Bool  "("  (Bool (Set  "the"  ($#u2_combgras :::"line-map"::: )  "of" (Set (Var "F"))) "is"   ($#v3_funct_2 :::"bijective"::: )  ) & (Bool (Set  "the"  ($#u1_combgras :::"point-map"::: )  "of" (Set (Var "F"))) "is"   ($#v3_funct_2 :::"bijective"::: )  ) & (Bool (Set (Var "F")) "is"   ($#v6_combgras :::"incidence_preserving"::: )  )  ")" )  ")" ))); 
 definitionlet "S1", "S2" be    ($#l1_incsp_1 :::"IncProjStr"::: )  ; let "F" be    ($#l1_combgras :::"IncProjMap"::: )   "over" (Set (Const "S1")) "," (Set (Const "S2")); let "K" be   ($#m1_subset_1 :::"Subset":::) "of" (Set  "the"  ($#u1_incsp_1 :::"Points"::: )  "of" (Set (Const "S1"))); func "F" :::".:"::: "K" ->   ($#m1_subset_1 :::"Subset":::) "of" (Set  "the"  ($#u1_incsp_1 :::"Points"::: )  "of" "S2") equals :: COMBGRAS:def 10 (Set (Set  "the"  ($#u1_combgras :::"point-map"::: )  "of" "F")  ($#k7_relat_1 :::".:"::: )  "K"); end; 








:: deftheorem    defines :::".:"::: COMBGRAS:def 10 :  (Bool  "for" (Set (Var "S1")) "," (Set (Var "S2")) "being"    ($#l1_incsp_1 :::"IncProjStr"::: )    (Bool  "for" (Set (Var "F")) "being"    ($#l1_combgras :::"IncProjMap"::: )   "over" (Set (Var "S1")) "," (Set (Var "S2"))  (Bool  "for" (Set (Var "K")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "the"  ($#u1_incsp_1 :::"Points"::: )  "of" (Set (Var "S1"))) "holds"  (Bool (Set (Set (Var "F"))  ($#k4_combgras :::".:"::: )  (Set (Var "K")))  ($#r1_hidden :::"="::: )  (Set (Set  "the"  ($#u1_combgras :::"point-map"::: )  "of" (Set (Var "F")))  ($#k7_relat_1 :::".:"::: )  (Set (Var "K"))))))); 
 definitionlet "S1", "S2" be    ($#l1_incsp_1 :::"IncProjStr"::: )  ; let "F" be    ($#l1_combgras :::"IncProjMap"::: )   "over" (Set (Const "S1")) "," (Set (Const "S2")); let "K" be   ($#m1_subset_1 :::"Subset":::) "of" (Set  "the"  ($#u1_incsp_1 :::"Points"::: )  "of" (Set (Const "S2"))); func "F" :::"""::: "K" ->   ($#m1_subset_1 :::"Subset":::) "of" (Set  "the"  ($#u1_incsp_1 :::"Points"::: )  "of" "S1") equals :: COMBGRAS:def 11 (Set (Set  "the"  ($#u1_combgras :::"point-map"::: )  "of" "F")  ($#k8_relat_1 :::"""::: )  "K"); end; 








:: deftheorem    defines :::"""::: COMBGRAS:def 11 :  (Bool  "for" (Set (Var "S1")) "," (Set (Var "S2")) "being"    ($#l1_incsp_1 :::"IncProjStr"::: )    (Bool  "for" (Set (Var "F")) "being"    ($#l1_combgras :::"IncProjMap"::: )   "over" (Set (Var "S1")) "," (Set (Var "S2"))  (Bool  "for" (Set (Var "K")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "the"  ($#u1_incsp_1 :::"Points"::: )  "of" (Set (Var "S2"))) "holds"  (Bool (Set (Set (Var "F"))  ($#k5_combgras :::"""::: )  (Set (Var "K")))  ($#r1_hidden :::"="::: )  (Set (Set  "the"  ($#u1_combgras :::"point-map"::: )  "of" (Set (Var "F")))  ($#k8_relat_1 :::"""::: )  (Set (Var "K"))))))); 
 definitionlet "X" be    ($#m1_hidden :::"set"::: )  ; let "A" be   ($#v1_finset_1 :::"finite"::: )     ($#m1_hidden :::"set"::: )  ; func  :::"^^":::  "(" "A" "," "X" ")"  ->   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k9_setfam_1 :::"bool"::: )  "X" ")" ) equals :: COMBGRAS:def 12  "{"  (Set (Var "B")) where B "is"   ($#m1_subset_1 :::"Subset":::) "of" "X" : (Bool  "("  (Bool (Set   ($#k1_card_1 :::"card"::: )  (Set (Var "B")))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k5_card_1 :::"card"::: )  "A" ")" )  ($#k2_nat_1 :::"+"::: )  (Num 1))) & (Bool "A"  ($#r1_tarski :::"c="::: )  (Set (Var "B")))  ")" )  "}"  ; end; 






:: deftheorem    defines :::"^^"::: COMBGRAS:def 12 :  (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "A")) "being"   ($#v1_finset_1 :::"finite"::: )     ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set   ($#k6_combgras :::"^^"::: )   "(" (Set (Var "A")) "," (Set (Var "X")) ")" )  ($#r1_hidden :::"="::: )   "{"  (Set (Var "B")) where B "is"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) : (Bool  "("  (Bool (Set   ($#k1_card_1 :::"card"::: )  (Set (Var "B")))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k5_card_1 :::"card"::: )  (Set (Var "A")) ")" )  ($#k2_nat_1 :::"+"::: )  (Num 1))) & (Bool (Set (Var "A"))  ($#r1_tarski :::"c="::: )  (Set (Var "B")))  ")" )  "}"  ))); 
 definitionlet "k" be    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ); let "X" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  ; assume 
(Bool  "("  (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set (Const "k"))) & (Bool (Set (Set (Const "k"))  ($#k2_nat_1 :::"+"::: )  (Num 1))  ($#r1_ordinal1 :::"c="::: )  (Set   ($#k1_card_1 :::"card"::: )  (Set (Const "X"))))  ")" )
 ; let "A" be   ($#v1_finset_1 :::"finite"::: )     ($#m1_hidden :::"set"::: )  ; assume 
(Bool (Set   ($#k5_card_1 :::"card"::: )  (Set (Const "A")))  ($#r1_hidden :::"="::: )  (Set (Set (Const "k"))  ($#k5_real_1 :::"-"::: )  (Num 1)))
 ; func  :::"^^":::  "(" "A" "," "X" "," "k" ")"  ->   ($#m1_subset_1 :::"Subset":::) "of" (Set  "the"  ($#u1_incsp_1 :::"Points"::: )  "of" (Set  "("  ($#k1_combgras :::"G_"::: )   "(" "k" "," "X" ")"  ")" )) equals :: COMBGRAS:def 13 (Set   ($#k6_combgras :::"^^"::: )   "(" "A" "," "X" ")" ); end; 








:: deftheorem    defines :::"^^"::: COMBGRAS:def 13 :  (Bool  "for" (Set (Var "k")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "X")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "k"))) & (Bool (Set (Set (Var "k"))  ($#k2_nat_1 :::"+"::: )  (Num 1))  ($#r1_ordinal1 :::"c="::: )  (Set   ($#k1_card_1 :::"card"::: )  (Set (Var "X"))))) "holds"  (Bool  "for" (Set (Var "A")) "being"   ($#v1_finset_1 :::"finite"::: )     ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set   ($#k5_card_1 :::"card"::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "k"))  ($#k5_real_1 :::"-"::: )  (Num 1)))) "holds"  (Bool (Set   ($#k7_combgras :::"^^"::: )   "(" (Set (Var "A")) "," (Set (Var "X")) "," (Set (Var "k")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k6_combgras :::"^^"::: )   "(" (Set (Var "A")) "," (Set (Var "X")) ")" ))))); 
 
theorem :: COMBGRAS:18 (Bool  "for" (Set (Var "S1")) "," (Set (Var "S2")) "being"    ($#l1_incsp_1 :::"IncProjStr"::: )    (Bool  "for" (Set (Var "F")) "being"    ($#l1_combgras :::"IncProjMap"::: )   "over" (Set (Var "S1")) "," (Set (Var "S2"))  (Bool  "for" (Set (Var "K")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "the"  ($#u1_incsp_1 :::"Points"::: )  "of" (Set (Var "S1"))) "holds"  (Bool (Set (Set (Var "F"))  ($#k4_combgras :::".:"::: )  (Set (Var "K")))  ($#r1_hidden :::"="::: )   "{"  (Set (Var "B")) where B "is"   ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "S2")) : (Bool  "ex" (Set (Var "A")) "being"   ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "S1")) "st"  (Bool  "("  (Bool (Set (Var "A"))  ($#r2_hidden :::"in"::: )  (Set (Var "K"))) & (Bool (Set (Set (Var "F"))  ($#k2_combgras :::"."::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set (Var "B")))  ")" ))  "}"  )))) ; 
 
theorem :: COMBGRAS:19 (Bool  "for" (Set (Var "S1")) "," (Set (Var "S2")) "being"    ($#l1_incsp_1 :::"IncProjStr"::: )    (Bool  "for" (Set (Var "F")) "being"    ($#l1_combgras :::"IncProjMap"::: )   "over" (Set (Var "S1")) "," (Set (Var "S2"))  (Bool  "for" (Set (Var "K")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "the"  ($#u1_incsp_1 :::"Points"::: )  "of" (Set (Var "S2"))) "holds"  (Bool (Set (Set (Var "F"))  ($#k5_combgras :::"""::: )  (Set (Var "K")))  ($#r1_hidden :::"="::: )   "{"  (Set (Var "A")) where A "is"   ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "S1")) : (Bool  "ex" (Set (Var "B")) "being"   ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "S2")) "st"  (Bool  "("  (Bool (Set (Var "B"))  ($#r2_hidden :::"in"::: )  (Set (Var "K"))) & (Bool (Set (Set (Var "F"))  ($#k2_combgras :::"."::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set (Var "B")))  ")" ))  "}"  )))) ; 
 
theorem :: COMBGRAS:20 (Bool  "for" (Set (Var "S")) "being"    ($#l1_incsp_1 :::"IncProjStr"::: )    (Bool  "for" (Set (Var "F")) "being"    ($#l1_combgras :::"IncProjMap"::: )   "over" (Set (Var "S")) "," (Set (Var "S"))  (Bool  "for" (Set (Var "K")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "the"  ($#u1_incsp_1 :::"Points"::: )  "of" (Set (Var "S")))  "st" (Bool (Bool (Set (Var "F")) "is"   ($#v6_combgras :::"incidence_preserving"::: )  ) & (Bool (Set (Var "K")) "is"   ($#v1_combgras :::"clique"::: )  )) "holds"  (Bool (Set (Set (Var "F"))  ($#k4_combgras :::".:"::: )  (Set (Var "K"))) "is"   ($#v1_combgras :::"clique"::: )  )))) ; 
 
theorem :: COMBGRAS:21 (Bool  "for" (Set (Var "S")) "being"    ($#l1_incsp_1 :::"IncProjStr"::: )    (Bool  "for" (Set (Var "F")) "being"    ($#l1_combgras :::"IncProjMap"::: )   "over" (Set (Var "S")) "," (Set (Var "S"))  (Bool  "for" (Set (Var "K")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "the"  ($#u1_incsp_1 :::"Points"::: )  "of" (Set (Var "S")))  "st" (Bool (Bool (Set (Var "F")) "is"   ($#v6_combgras :::"incidence_preserving"::: )  ) & (Bool (Set  "the"  ($#u2_combgras :::"line-map"::: )  "of" (Set (Var "F"))) "is"   ($#v2_funct_2 :::"onto"::: )  ) & (Bool (Set (Var "K")) "is"   ($#v1_combgras :::"clique"::: )  )) "holds"  (Bool (Set (Set (Var "F"))  ($#k5_combgras :::"""::: )  (Set (Var "K"))) "is"   ($#v1_combgras :::"clique"::: )  )))) ; 
 
theorem :: COMBGRAS:22 (Bool  "for" (Set (Var "S")) "being"    ($#l1_incsp_1 :::"IncProjStr"::: )    (Bool  "for" (Set (Var "F")) "being"    ($#l1_combgras :::"IncProjMap"::: )   "over" (Set (Var "S")) "," (Set (Var "S"))  (Bool  "for" (Set (Var "K")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "the"  ($#u1_incsp_1 :::"Points"::: )  "of" (Set (Var "S")))  "st" (Bool (Bool (Set (Var "F")) "is"   ($#v7_combgras :::"automorphism"::: )  ) & (Bool (Set (Var "K")) "is"   ($#v2_combgras :::"maximal_clique"::: )  )) "holds"  (Bool  "("  (Bool (Set (Set (Var "F"))  ($#k4_combgras :::".:"::: )  (Set (Var "K"))) "is"   ($#v2_combgras :::"maximal_clique"::: )  ) & (Bool (Set (Set (Var "F"))  ($#k5_combgras :::"""::: )  (Set (Var "K"))) "is"   ($#v2_combgras :::"maximal_clique"::: )  )  ")" )))) ; 
 
theorem :: COMBGRAS:23 (Bool  "for" (Set (Var "k")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "X")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Num 2)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "k"))) & (Bool (Set (Set (Var "k"))  ($#k2_nat_1 :::"+"::: )  (Num 2))  ($#r1_ordinal1 :::"c="::: )  (Set   ($#k1_card_1 :::"card"::: )  (Set (Var "X"))))) "holds"  (Bool  "for" (Set (Var "F")) "being"    ($#l1_combgras :::"IncProjMap"::: )   "over" (Set   ($#k1_combgras :::"G_"::: )   "(" (Set (Var "k")) "," (Set (Var "X")) ")" ) "," (Set   ($#k1_combgras :::"G_"::: )   "(" (Set (Var "k")) "," (Set (Var "X")) ")" )  "st" (Bool (Bool (Set (Var "F")) "is"   ($#v7_combgras :::"automorphism"::: )  )) "holds"  (Bool  "for" (Set (Var "K")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "the"  ($#u1_incsp_1 :::"Points"::: )  "of" (Set  "("  ($#k1_combgras :::"G_"::: )   "(" (Set (Var "k")) "," (Set (Var "X")) ")"  ")" ))  "st" (Bool (Bool (Set (Var "K")) "is"   ($#v3_combgras :::"STAR"::: )  )) "holds"  (Bool  "("  (Bool (Set (Set (Var "F"))  ($#k4_combgras :::".:"::: )  (Set (Var "K"))) "is"   ($#v3_combgras :::"STAR"::: )  ) & (Bool (Set (Set (Var "F"))  ($#k5_combgras :::"""::: )  (Set (Var "K"))) "is"   ($#v3_combgras :::"STAR"::: )  )  ")" ))))) ; 
 definitionlet "k" be    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ); let "X" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  ; assume 
(Bool  "("  (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set (Const "k"))) & (Bool (Set (Set (Const "k"))  ($#k2_nat_1 :::"+"::: )  (Num 1))  ($#r1_ordinal1 :::"c="::: )  (Set   ($#k1_card_1 :::"card"::: )  (Set (Const "X"))))  ")" )
 ; let "s" be   ($#m1_subset_1 :::"Permutation":::) "of" (Set (Const "X")); func  :::"incprojmap":::  "(" "k" "," "s" ")"  ->   ($#v5_combgras :::"strict"::: )     ($#l1_combgras :::"IncProjMap"::: )   "over" (Set   ($#k1_combgras :::"G_"::: )   "(" "k" "," "X" ")" ) "," (Set   ($#k1_combgras :::"G_"::: )   "(" "k" "," "X" ")" ) means :: COMBGRAS:def 14 (Bool  "("  (Bool  "("   "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"POINT":::) "of" (Set  "("  ($#k1_combgras :::"G_"::: )   "(" "k" "," "X" ")"  ")" ) "holds"  (Bool (Set it  ($#k2_combgras :::"."::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set "s"  ($#k7_relat_1 :::".:"::: )  (Set (Var "A"))))  ")" ) & (Bool  "("   "for" (Set (Var "L")) "being"   ($#m1_subset_1 :::"LINE":::) "of" (Set  "("  ($#k1_combgras :::"G_"::: )   "(" "k" "," "X" ")"  ")" ) "holds"  (Bool (Set it  ($#k3_combgras :::"."::: )  (Set (Var "L")))  ($#r1_hidden :::"="::: )  (Set "s"  ($#k7_relat_1 :::".:"::: )  (Set (Var "L"))))  ")" )  ")" ); end; 








:: deftheorem    defines :::"incprojmap"::: COMBGRAS:def 14 :  (Bool  "for" (Set (Var "k")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "X")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "k"))) & (Bool (Set (Set (Var "k"))  ($#k2_nat_1 :::"+"::: )  (Num 1))  ($#r1_ordinal1 :::"c="::: )  (Set   ($#k1_card_1 :::"card"::: )  (Set (Var "X"))))) "holds"  (Bool  "for" (Set (Var "s")) "being"   ($#m1_subset_1 :::"Permutation":::) "of" (Set (Var "X"))  (Bool  "for" (Set (Var "b4")) "being"   ($#v5_combgras :::"strict"::: )     ($#l1_combgras :::"IncProjMap"::: )   "over" (Set   ($#k1_combgras :::"G_"::: )   "(" (Set (Var "k")) "," (Set (Var "X")) ")" ) "," (Set   ($#k1_combgras :::"G_"::: )   "(" (Set (Var "k")) "," (Set (Var "X")) ")" ) "holds"   (Bool  "("  (Bool (Set (Var "b4"))  ($#r1_hidden :::"="::: )  (Set   ($#k8_combgras :::"incprojmap"::: )   "(" (Set (Var "k")) "," (Set (Var "s")) ")" )) "iff" (Bool  "("  (Bool  "("   "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"POINT":::) "of" (Set  "("  ($#k1_combgras :::"G_"::: )   "(" (Set (Var "k")) "," (Set (Var "X")) ")"  ")" ) "holds"  (Bool (Set (Set (Var "b4"))  ($#k2_combgras :::"."::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "s"))  ($#k7_relat_1 :::".:"::: )  (Set (Var "A"))))  ")" ) & (Bool  "("   "for" (Set (Var "L")) "being"   ($#m1_subset_1 :::"LINE":::) "of" (Set  "("  ($#k1_combgras :::"G_"::: )   "(" (Set (Var "k")) "," (Set (Var "X")) ")"  ")" ) "holds"  (Bool (Set (Set (Var "b4"))  ($#k3_combgras :::"."::: )  (Set (Var "L")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "s"))  ($#k7_relat_1 :::".:"::: )  (Set (Var "L"))))  ")" )  ")" )  ")" ))))); 
 
theorem :: COMBGRAS:24 (Bool  "for" (Set (Var "k")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "X")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "k"))  ($#r1_hidden :::"="::: )  (Num 1)) & (Bool (Set (Set (Var "k"))  ($#k2_nat_1 :::"+"::: )  (Num 1))  ($#r1_ordinal1 :::"c="::: )  (Set   ($#k1_card_1 :::"card"::: )  (Set (Var "X"))))) "holds"  (Bool  "for" (Set (Var "F")) "being"    ($#l1_combgras :::"IncProjMap"::: )   "over" (Set   ($#k1_combgras :::"G_"::: )   "(" (Set (Var "k")) "," (Set (Var "X")) ")" ) "," (Set   ($#k1_combgras :::"G_"::: )   "(" (Set (Var "k")) "," (Set (Var "X")) ")" )  "st" (Bool (Bool (Set (Var "F")) "is"   ($#v7_combgras :::"automorphism"::: )  )) "holds"  (Bool  "ex" (Set (Var "s")) "being"   ($#m1_subset_1 :::"Permutation":::) "of" (Set (Var "X")) "st" (Bool (Set   ($#g1_combgras :::"IncProjMap"::: )  "(#"  (Set  "the"  ($#u1_combgras :::"point-map"::: )  "of" (Set (Var "F"))) "," (Set  "the"  ($#u2_combgras :::"line-map"::: )  "of" (Set (Var "F"))) "#)" )  ($#r1_hidden :::"="::: )  (Set   ($#k8_combgras :::"incprojmap"::: )   "(" (Set (Var "k")) "," (Set (Var "s")) ")" )))))) ; 
 
theorem :: COMBGRAS:25 (Bool  "for" (Set (Var "k")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "X")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "k"))) & (Bool (Set   ($#k1_card_1 :::"card"::: )  (Set (Var "X")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "k"))  ($#k2_nat_1 :::"+"::: )  (Num 1)))) "holds"  (Bool  "for" (Set (Var "F")) "being"    ($#l1_combgras :::"IncProjMap"::: )   "over" (Set   ($#k1_combgras :::"G_"::: )   "(" (Set (Var "k")) "," (Set (Var "X")) ")" ) "," (Set   ($#k1_combgras :::"G_"::: )   "(" (Set (Var "k")) "," (Set (Var "X")) ")" )  "st" (Bool (Bool (Set (Var "F")) "is"   ($#v7_combgras :::"automorphism"::: )  )) "holds"  (Bool  "ex" (Set (Var "s")) "being"   ($#m1_subset_1 :::"Permutation":::) "of" (Set (Var "X")) "st" (Bool (Set   ($#g1_combgras :::"IncProjMap"::: )  "(#"  (Set  "the"  ($#u1_combgras :::"point-map"::: )  "of" (Set (Var "F"))) "," (Set  "the"  ($#u2_combgras :::"line-map"::: )  "of" (Set (Var "F"))) "#)" )  ($#r1_hidden :::"="::: )  (Set   ($#k8_combgras :::"incprojmap"::: )   "(" (Set (Var "k")) "," (Set (Var "s")) ")" )))))) ; 
 
theorem :: COMBGRAS:26 (Bool  "for" (Set (Var "k")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "X")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "k"))) & (Bool (Set (Set (Var "k"))  ($#k2_nat_1 :::"+"::: )  (Num 1))  ($#r1_ordinal1 :::"c="::: )  (Set   ($#k1_card_1 :::"card"::: )  (Set (Var "X"))))) "holds"  (Bool  "for" (Set (Var "T")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "the"  ($#u1_incsp_1 :::"Points"::: )  "of" (Set  "("  ($#k1_combgras :::"G_"::: )   "(" (Set (Var "k")) "," (Set (Var "X")) ")"  ")" ))  (Bool  "for" (Set (Var "S")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X"))  "st" (Bool (Bool (Set   ($#k1_card_1 :::"card"::: )  (Set (Var "S")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "k"))  ($#k5_real_1 :::"-"::: )  (Num 1))) & (Bool (Set (Var "T"))  ($#r1_hidden :::"="::: )   "{"  (Set (Var "A")) where A "is"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) : (Bool  "("  (Bool (Set   ($#k1_card_1 :::"card"::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set (Var "k"))) & (Bool (Set (Var "S"))  ($#r1_tarski :::"c="::: )  (Set (Var "A")))  ")" )  "}"  )) "holds"  (Bool (Set (Var "S"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_setfam_1 :::"meet"::: )  (Set (Var "T")))))))) ; 
 
theorem :: COMBGRAS:27 (Bool  "for" (Set (Var "k")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "X")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "k"))) & (Bool (Set (Set (Var "k"))  ($#k2_nat_1 :::"+"::: )  (Num 1))  ($#r1_ordinal1 :::"c="::: )  (Set   ($#k1_card_1 :::"card"::: )  (Set (Var "X"))))) "holds"  (Bool  "for" (Set (Var "T")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "the"  ($#u1_incsp_1 :::"Points"::: )  "of" (Set  "("  ($#k1_combgras :::"G_"::: )   "(" (Set (Var "k")) "," (Set (Var "X")) ")"  ")" ))  "st" (Bool (Bool (Set (Var "T")) "is"   ($#v3_combgras :::"STAR"::: )  )) "holds"  (Bool  "for" (Set (Var "S")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X"))  "st" (Bool (Bool (Set (Var "S"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_setfam_1 :::"meet"::: )  (Set (Var "T"))))) "holds"  (Bool  "("  (Bool (Set   ($#k1_card_1 :::"card"::: )  (Set (Var "S")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "k"))  ($#k5_real_1 :::"-"::: )  (Num 1))) & (Bool (Set (Var "T"))  ($#r1_hidden :::"="::: )   "{"  (Set (Var "A")) where A "is"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) : (Bool  "("  (Bool (Set   ($#k1_card_1 :::"card"::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set (Var "k"))) & (Bool (Set (Var "S"))  ($#r1_tarski :::"c="::: )  (Set (Var "A")))  ")" )  "}"  )  ")" ))))) ; 
 
theorem :: COMBGRAS:28 (Bool  "for" (Set (Var "k")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "X")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "k"))) & (Bool (Set (Set (Var "k"))  ($#k2_nat_1 :::"+"::: )  (Num 1))  ($#r1_ordinal1 :::"c="::: )  (Set   ($#k1_card_1 :::"card"::: )  (Set (Var "X"))))) "holds"  (Bool  "for" (Set (Var "T1")) "," (Set (Var "T2")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "the"  ($#u1_incsp_1 :::"Points"::: )  "of" (Set  "("  ($#k1_combgras :::"G_"::: )   "(" (Set (Var "k")) "," (Set (Var "X")) ")"  ")" ))  "st" (Bool (Bool (Set (Var "T1")) "is"   ($#v3_combgras :::"STAR"::: )  ) & (Bool (Set (Var "T2")) "is"   ($#v3_combgras :::"STAR"::: )  ) & (Bool (Set   ($#k1_setfam_1 :::"meet"::: )  (Set (Var "T1")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_setfam_1 :::"meet"::: )  (Set (Var "T2"))))) "holds"  (Bool (Set (Var "T1"))  ($#r1_hidden :::"="::: )  (Set (Var "T2")))))) ; 
 
theorem :: COMBGRAS:29 (Bool  "for" (Set (Var "k")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "X")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Set (Var "k"))  ($#k2_nat_1 :::"+"::: )  (Num 1))  ($#r1_ordinal1 :::"c="::: )  (Set   ($#k1_card_1 :::"card"::: )  (Set (Var "X"))))) "holds"  (Bool  "for" (Set (Var "A")) "being"   ($#v1_finset_1 :::"finite"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X"))  "st" (Bool (Bool (Set   ($#k5_card_1 :::"card"::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "k"))  ($#k5_real_1 :::"-"::: )  (Num 1)))) "holds"  (Bool (Set   ($#k7_combgras :::"^^"::: )   "(" (Set (Var "A")) "," (Set (Var "X")) "," (Set (Var "k")) ")" ) "is"   ($#v3_combgras :::"STAR"::: )  )))) ; 
 
theorem :: COMBGRAS:30 (Bool  "for" (Set (Var "k")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "X")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Set (Var "k"))  ($#k2_nat_1 :::"+"::: )  (Num 1))  ($#r1_ordinal1 :::"c="::: )  (Set   ($#k1_card_1 :::"card"::: )  (Set (Var "X"))))) "holds"  (Bool  "for" (Set (Var "A")) "being"   ($#v1_finset_1 :::"finite"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X"))  "st" (Bool (Bool (Set   ($#k5_card_1 :::"card"::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "k"))  ($#k5_real_1 :::"-"::: )  (Num 1)))) "holds"  (Bool (Set   ($#k1_setfam_1 :::"meet"::: )  (Set  "("  ($#k7_combgras :::"^^"::: )   "(" (Set (Var "A")) "," (Set (Var "X")) "," (Set (Var "k")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "A")))))) ; 
 
theorem :: COMBGRAS:31 (Bool  "for" (Set (Var "k")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "X")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "k"))) & (Bool (Set (Set (Var "k"))  ($#k2_nat_1 :::"+"::: )  (Num 3))  ($#r1_ordinal1 :::"c="::: )  (Set   ($#k1_card_1 :::"card"::: )  (Set (Var "X"))))) "holds"  (Bool  "for" (Set (Var "F")) "being"    ($#l1_combgras :::"IncProjMap"::: )   "over" (Set   ($#k1_combgras :::"G_"::: )   "(" (Set  "(" (Set (Var "k"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) "," (Set (Var "X")) ")" ) "," (Set   ($#k1_combgras :::"G_"::: )   "(" (Set  "(" (Set (Var "k"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) "," (Set (Var "X")) ")" )  "st" (Bool (Bool (Set (Var "F")) "is"   ($#v7_combgras :::"automorphism"::: )  )) "holds"  (Bool  "ex" (Set (Var "H")) "being"    ($#l1_combgras :::"IncProjMap"::: )   "over" (Set   ($#k1_combgras :::"G_"::: )   "(" (Set (Var "k")) "," (Set (Var "X")) ")" ) "," (Set   ($#k1_combgras :::"G_"::: )   "(" (Set (Var "k")) "," (Set (Var "X")) ")" ) "st"  (Bool  "("  (Bool (Set (Var "H")) "is"   ($#v7_combgras :::"automorphism"::: )  ) & (Bool (Set  "the"  ($#u2_combgras :::"line-map"::: )  "of" (Set (Var "H")))  ($#r1_funct_2 :::"="::: )  (Set  "the"  ($#u1_combgras :::"point-map"::: )  "of" (Set (Var "F")))) & (Bool  "("   "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"POINT":::) "of" (Set  "("  ($#k1_combgras :::"G_"::: )   "(" (Set (Var "k")) "," (Set (Var "X")) ")"  ")" )  (Bool  "for" (Set (Var "B")) "being"   ($#v1_finset_1 :::"finite"::: )     ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "B"))  ($#r1_hidden :::"="::: )  (Set (Var "A")))) "holds"  (Bool (Set (Set (Var "H"))  ($#k2_combgras :::"."::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_setfam_1 :::"meet"::: )  (Set  "(" (Set (Var "F"))  ($#k4_combgras :::".:"::: )  (Set  "("  ($#k7_combgras :::"^^"::: )   "(" (Set (Var "B")) "," (Set (Var "X")) "," (Set  "(" (Set (Var "k"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) ")"  ")" ) ")" ))))  ")" )  ")" ))))) ; 
 
theorem :: COMBGRAS:32 (Bool  "for" (Set (Var "k")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "X")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "k"))) & (Bool (Set (Set (Var "k"))  ($#k2_nat_1 :::"+"::: )  (Num 3))  ($#r1_ordinal1 :::"c="::: )  (Set   ($#k1_card_1 :::"card"::: )  (Set (Var "X"))))) "holds"  (Bool  "for" (Set (Var "F")) "being"    ($#l1_combgras :::"IncProjMap"::: )   "over" (Set   ($#k1_combgras :::"G_"::: )   "(" (Set  "(" (Set (Var "k"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) "," (Set (Var "X")) ")" ) "," (Set   ($#k1_combgras :::"G_"::: )   "(" (Set  "(" (Set (Var "k"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) "," (Set (Var "X")) ")" )  "st" (Bool (Bool (Set (Var "F")) "is"   ($#v7_combgras :::"automorphism"::: )  )) "holds"  (Bool  "for" (Set (Var "H")) "being"    ($#l1_combgras :::"IncProjMap"::: )   "over" (Set   ($#k1_combgras :::"G_"::: )   "(" (Set (Var "k")) "," (Set (Var "X")) ")" ) "," (Set   ($#k1_combgras :::"G_"::: )   "(" (Set (Var "k")) "," (Set (Var "X")) ")" )  "st" (Bool (Bool (Set  "the"  ($#u2_combgras :::"line-map"::: )  "of" (Set (Var "H")))  ($#r1_funct_2 :::"="::: )  (Set  "the"  ($#u1_combgras :::"point-map"::: )  "of" (Set (Var "F"))))) "holds"  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Permutation":::) "of" (Set (Var "X"))  "st" (Bool (Bool (Set   ($#g1_combgras :::"IncProjMap"::: )  "(#"  (Set  "the"  ($#u1_combgras :::"point-map"::: )  "of" (Set (Var "H"))) "," (Set  "the"  ($#u2_combgras :::"line-map"::: )  "of" (Set (Var "H"))) "#)" )  ($#r1_hidden :::"="::: )  (Set   ($#k8_combgras :::"incprojmap"::: )   "(" (Set (Var "k")) "," (Set (Var "f")) ")" ))) "holds"  (Bool (Set   ($#g1_combgras :::"IncProjMap"::: )  "(#"  (Set  "the"  ($#u1_combgras :::"point-map"::: )  "of" (Set (Var "F"))) "," (Set  "the"  ($#u2_combgras :::"line-map"::: )  "of" (Set (Var "F"))) "#)" )  ($#r1_hidden :::"="::: )  (Set   ($#k8_combgras :::"incprojmap"::: )   "(" (Set  "(" (Set (Var "k"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) "," (Set (Var "f")) ")" ))))))) ; 
 
theorem :: COMBGRAS:33 (Bool  "for" (Set (Var "k")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "X")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Num 2)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "k"))) & (Bool (Set (Set (Var "k"))  ($#k2_nat_1 :::"+"::: )  (Num 2))  ($#r1_ordinal1 :::"c="::: )  (Set   ($#k1_card_1 :::"card"::: )  (Set (Var "X"))))) "holds"  (Bool  "for" (Set (Var "F")) "being"    ($#l1_combgras :::"IncProjMap"::: )   "over" (Set   ($#k1_combgras :::"G_"::: )   "(" (Set (Var "k")) "," (Set (Var "X")) ")" ) "," (Set   ($#k1_combgras :::"G_"::: )   "(" (Set (Var "k")) "," (Set (Var "X")) ")" )  "st" (Bool (Bool (Set (Var "F")) "is"   ($#v7_combgras :::"automorphism"::: )  )) "holds"  (Bool  "ex" (Set (Var "s")) "being"   ($#m1_subset_1 :::"Permutation":::) "of" (Set (Var "X")) "st" (Bool (Set   ($#g1_combgras :::"IncProjMap"::: )  "(#"  (Set  "the"  ($#u1_combgras :::"point-map"::: )  "of" (Set (Var "F"))) "," (Set  "the"  ($#u2_combgras :::"line-map"::: )  "of" (Set (Var "F"))) "#)" )  ($#r1_hidden :::"="::: )  (Set   ($#k8_combgras :::"incprojmap"::: )   "(" (Set (Var "k")) "," (Set (Var "s")) ")" )))))) ; 
 
theorem :: COMBGRAS:34 (Bool  "for" (Set (Var "k")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "X")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "k"))) & (Bool (Set (Set (Var "k"))  ($#k2_nat_1 :::"+"::: )  (Num 1))  ($#r1_ordinal1 :::"c="::: )  (Set   ($#k1_card_1 :::"card"::: )  (Set (Var "X"))))) "holds"  (Bool  "for" (Set (Var "s")) "being"   ($#m1_subset_1 :::"Permutation":::) "of" (Set (Var "X")) "holds"  (Bool (Set   ($#k8_combgras :::"incprojmap"::: )   "(" (Set (Var "k")) "," (Set (Var "s")) ")" ) "is"   ($#v7_combgras :::"automorphism"::: )  )))) ; 
 
theorem :: COMBGRAS:35 (Bool  "for" (Set (Var "k")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "X")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "k"))) & (Bool (Set (Set (Var "k"))  ($#k2_nat_1 :::"+"::: )  (Num 1))  ($#r1_ordinal1 :::"c="::: )  (Set   ($#k1_card_1 :::"card"::: )  (Set (Var "X"))))) "holds"  (Bool  "for" (Set (Var "F")) "being"    ($#l1_combgras :::"IncProjMap"::: )   "over" (Set   ($#k1_combgras :::"G_"::: )   "(" (Set (Var "k")) "," (Set (Var "X")) ")" ) "," (Set   ($#k1_combgras :::"G_"::: )   "(" (Set (Var "k")) "," (Set (Var "X")) ")" ) "holds"   (Bool  "("  (Bool (Set (Var "F")) "is"   ($#v7_combgras :::"automorphism"::: )  ) "iff" (Bool  "ex" (Set (Var "s")) "being"   ($#m1_subset_1 :::"Permutation":::) "of" (Set (Var "X")) "st" (Bool (Set   ($#g1_combgras :::"IncProjMap"::: )  "(#"  (Set  "the"  ($#u1_combgras :::"point-map"::: )  "of" (Set (Var "F"))) "," (Set  "the"  ($#u2_combgras :::"line-map"::: )  "of" (Set (Var "F"))) "#)" )  ($#r1_hidden :::"="::: )  (Set   ($#k8_combgras :::"incprojmap"::: )   "(" (Set (Var "k")) "," (Set (Var "s")) ")" )))  ")" )))) ;