:: INCSP_1  semantic presentation begin  definitionattr "c1" is  :::"strict"::: ; struct  :::"IncProjStr":::  -> ; aggr :::"IncProjStr":::(# :::"Points":::, :::"Lines":::, :::"Inc"::: #) ->    ($#l1_incsp_1 :::"IncProjStr"::: )  ; sel  :::"Points"::: "c1" ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  ; sel  :::"Lines"::: "c1" ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  ; sel  :::"Inc"::: "c1" ->   ($#m1_subset_1 :::"Relation":::) "of" (Set  "the"  ($#u1_incsp_1 :::"Points"::: )  "of" "c1") "," (Set  "the"  ($#u2_incsp_1 :::"Lines"::: )  "of" "c1"); end; definitionattr "c1" is  :::"strict"::: ; struct  :::"IncStruct":::  ->    ($#l1_incsp_1 :::"IncProjStr"::: )  ; aggr :::"IncStruct":::(# :::"Points":::, :::"Lines":::, :::"Planes":::, :::"Inc":::, :::"Inc2":::, :::"Inc3"::: #) ->    ($#l2_incsp_1 :::"IncStruct"::: )  ; sel  :::"Planes"::: "c1" ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  ; sel  :::"Inc2"::: "c1" ->   ($#m1_subset_1 :::"Relation":::) "of" (Set  "the"  ($#u1_incsp_1 :::"Points"::: )  "of" "c1") "," (Set  "the"  ($#u4_incsp_1 :::"Planes"::: )  "of" "c1"); sel  :::"Inc3"::: "c1" ->   ($#m1_subset_1 :::"Relation":::) "of" (Set  "the"  ($#u2_incsp_1 :::"Lines"::: )  "of" "c1") "," (Set  "the"  ($#u4_incsp_1 :::"Planes"::: )  "of" "c1"); end; definitionlet "S" be    ($#l1_incsp_1 :::"IncProjStr"::: )  ; mode POINT of "S" is    ($#m1_subset_1 :::"Element"::: )   "of" (Set  "the"  ($#u1_incsp_1 :::"Points"::: )  "of" "S"); mode LINE of "S" is    ($#m1_subset_1 :::"Element"::: )   "of" (Set  "the"  ($#u2_incsp_1 :::"Lines"::: )  "of" "S"); end; definitionlet "S" be    ($#l2_incsp_1 :::"IncStruct"::: )  ; mode PLANE of "S" is    ($#m1_subset_1 :::"Element"::: )   "of" (Set  "the"  ($#u4_incsp_1 :::"Planes"::: )  "of" "S"); end; 


















definitionlet "S" be    ($#l1_incsp_1 :::"IncProjStr"::: )  ; let "A" be   ($#m1_subset_1 :::"POINT":::) "of" (Set (Const "S")); let "L" be   ($#m1_subset_1 :::"LINE":::) "of" (Set (Const "S")); pred "A" :::"on"::: "L" means :: INCSP_1:def 1 (Bool (Set  ($#k1_domain_1 :::"["::: ) "A" "," "L" ($#k1_domain_1 :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set  "the"  ($#u3_incsp_1 :::"Inc"::: )  "of" "S")); end; 






:: deftheorem    defines :::"on"::: INCSP_1:def 1 :  (Bool  "for" (Set (Var "S")) "being"    ($#l1_incsp_1 :::"IncProjStr"::: )    (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "S"))  (Bool  "for" (Set (Var "L")) "being"   ($#m1_subset_1 :::"LINE":::) "of" (Set (Var "S")) "holds"   (Bool  "("  (Bool (Set (Var "A"))  ($#r1_incsp_1 :::"on"::: )  (Set (Var "L"))) "iff" (Bool (Set  ($#k1_domain_1 :::"["::: ) (Set (Var "A")) "," (Set (Var "L")) ($#k1_domain_1 :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set  "the"  ($#u3_incsp_1 :::"Inc"::: )  "of" (Set (Var "S"))))  ")" )))); 
 definitionlet "S" be    ($#l2_incsp_1 :::"IncStruct"::: )  ; let "A" be   ($#m1_subset_1 :::"POINT":::) "of" (Set (Const "S")); let "P" be   ($#m1_subset_1 :::"PLANE":::) "of" (Set (Const "S")); pred "A" :::"on"::: "P" means :: INCSP_1:def 2 (Bool (Set  ($#k1_domain_1 :::"["::: ) "A" "," "P" ($#k1_domain_1 :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set  "the"  ($#u5_incsp_1 :::"Inc2"::: )  "of" "S")); end; 






:: deftheorem    defines :::"on"::: INCSP_1:def 2 :  (Bool  "for" (Set (Var "S")) "being"    ($#l2_incsp_1 :::"IncStruct"::: )    (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "S"))  (Bool  "for" (Set (Var "P")) "being"   ($#m1_subset_1 :::"PLANE":::) "of" (Set (Var "S")) "holds"   (Bool  "("  (Bool (Set (Var "A"))  ($#r2_incsp_1 :::"on"::: )  (Set (Var "P"))) "iff" (Bool (Set  ($#k1_domain_1 :::"["::: ) (Set (Var "A")) "," (Set (Var "P")) ($#k1_domain_1 :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set  "the"  ($#u5_incsp_1 :::"Inc2"::: )  "of" (Set (Var "S"))))  ")" )))); 
 definitionlet "S" be    ($#l2_incsp_1 :::"IncStruct"::: )  ; let "L" be   ($#m1_subset_1 :::"LINE":::) "of" (Set (Const "S")); let "P" be   ($#m1_subset_1 :::"PLANE":::) "of" (Set (Const "S")); pred "L" :::"on"::: "P" means :: INCSP_1:def 3 (Bool (Set  ($#k1_domain_1 :::"["::: ) "L" "," "P" ($#k1_domain_1 :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set  "the"  ($#u6_incsp_1 :::"Inc3"::: )  "of" "S")); end; 






:: deftheorem    defines :::"on"::: INCSP_1:def 3 :  (Bool  "for" (Set (Var "S")) "being"    ($#l2_incsp_1 :::"IncStruct"::: )    (Bool  "for" (Set (Var "L")) "being"   ($#m1_subset_1 :::"LINE":::) "of" (Set (Var "S"))  (Bool  "for" (Set (Var "P")) "being"   ($#m1_subset_1 :::"PLANE":::) "of" (Set (Var "S")) "holds"   (Bool  "("  (Bool (Set (Var "L"))  ($#r3_incsp_1 :::"on"::: )  (Set (Var "P"))) "iff" (Bool (Set  ($#k1_domain_1 :::"["::: ) (Set (Var "L")) "," (Set (Var "P")) ($#k1_domain_1 :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set  "the"  ($#u6_incsp_1 :::"Inc3"::: )  "of" (Set (Var "S"))))  ")" )))); 
 definitionlet "S" be    ($#l1_incsp_1 :::"IncProjStr"::: )  ; let "F" be   ($#m1_subset_1 :::"Subset":::) "of" (Set  "the"  ($#u1_incsp_1 :::"Points"::: )  "of" (Set (Const "S"))); let "L" be   ($#m1_subset_1 :::"LINE":::) "of" (Set (Const "S")); pred "F" :::"on"::: "L" means :: INCSP_1:def 4 (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"POINT":::) "of" "S"  "st" (Bool (Bool (Set (Var "A"))  ($#r2_hidden :::"in"::: )  "F")) "holds"  (Bool (Set (Var "A"))  ($#r1_incsp_1 :::"on"::: )  "L")); end; 






:: deftheorem    defines :::"on"::: INCSP_1:def 4 :  (Bool  "for" (Set (Var "S")) "being"    ($#l1_incsp_1 :::"IncProjStr"::: )    (Bool  "for" (Set (Var "F")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "the"  ($#u1_incsp_1 :::"Points"::: )  "of" (Set (Var "S")))  (Bool  "for" (Set (Var "L")) "being"   ($#m1_subset_1 :::"LINE":::) "of" (Set (Var "S")) "holds"   (Bool  "("  (Bool (Set (Var "F"))  ($#r4_incsp_1 :::"on"::: )  (Set (Var "L"))) "iff" (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "S"))  "st" (Bool (Bool (Set (Var "A"))  ($#r2_hidden :::"in"::: )  (Set (Var "F")))) "holds"  (Bool (Set (Var "A"))  ($#r1_incsp_1 :::"on"::: )  (Set (Var "L"))))  ")" )))); 
 definitionlet "S" be    ($#l2_incsp_1 :::"IncStruct"::: )  ; let "F" be   ($#m1_subset_1 :::"Subset":::) "of" (Set  "the"  ($#u1_incsp_1 :::"Points"::: )  "of" (Set (Const "S"))); let "P" be   ($#m1_subset_1 :::"PLANE":::) "of" (Set (Const "S")); pred "F" :::"on"::: "P" means :: INCSP_1:def 5 (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"POINT":::) "of" "S"  "st" (Bool (Bool (Set (Var "A"))  ($#r2_hidden :::"in"::: )  "F")) "holds"  (Bool (Set (Var "A"))  ($#r2_incsp_1 :::"on"::: )  "P")); end; 






:: deftheorem    defines :::"on"::: INCSP_1:def 5 :  (Bool  "for" (Set (Var "S")) "being"    ($#l2_incsp_1 :::"IncStruct"::: )    (Bool  "for" (Set (Var "F")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "the"  ($#u1_incsp_1 :::"Points"::: )  "of" (Set (Var "S")))  (Bool  "for" (Set (Var "P")) "being"   ($#m1_subset_1 :::"PLANE":::) "of" (Set (Var "S")) "holds"   (Bool  "("  (Bool (Set (Var "F"))  ($#r5_incsp_1 :::"on"::: )  (Set (Var "P"))) "iff" (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "S"))  "st" (Bool (Bool (Set (Var "A"))  ($#r2_hidden :::"in"::: )  (Set (Var "F")))) "holds"  (Bool (Set (Var "A"))  ($#r2_incsp_1 :::"on"::: )  (Set (Var "P"))))  ")" )))); 
 definitionlet "S" be    ($#l1_incsp_1 :::"IncProjStr"::: )  ; let "F" be   ($#m1_subset_1 :::"Subset":::) "of" (Set  "the"  ($#u1_incsp_1 :::"Points"::: )  "of" (Set (Const "S"))); attr "F" is  :::"linear":::  means :: INCSP_1:def 6 (Bool  "ex" (Set (Var "L")) "being"   ($#m1_subset_1 :::"LINE":::) "of" "S" "st" (Bool "F"  ($#r4_incsp_1 :::"on"::: )  (Set (Var "L")))); end; 





:: deftheorem    defines :::"linear"::: INCSP_1:def 6 :  (Bool  "for" (Set (Var "S")) "being"    ($#l1_incsp_1 :::"IncProjStr"::: )    (Bool  "for" (Set (Var "F")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "the"  ($#u1_incsp_1 :::"Points"::: )  "of" (Set (Var "S"))) "holds"   (Bool  "("  (Bool (Set (Var "F")) "is"   ($#v3_incsp_1 :::"linear"::: )  ) "iff" (Bool  "ex" (Set (Var "L")) "being"   ($#m1_subset_1 :::"LINE":::) "of" (Set (Var "S")) "st" (Bool (Set (Var "F"))  ($#r4_incsp_1 :::"on"::: )  (Set (Var "L"))))  ")" ))); 
 definitionlet "S" be    ($#l2_incsp_1 :::"IncStruct"::: )  ; let "F" be   ($#m1_subset_1 :::"Subset":::) "of" (Set  "the"  ($#u1_incsp_1 :::"Points"::: )  "of" (Set (Const "S"))); attr "F" is  :::"planar":::  means :: INCSP_1:def 7 (Bool  "ex" (Set (Var "P")) "being"   ($#m1_subset_1 :::"PLANE":::) "of" "S" "st" (Bool "F"  ($#r5_incsp_1 :::"on"::: )  (Set (Var "P")))); end; 





:: deftheorem    defines :::"planar"::: INCSP_1:def 7 :  (Bool  "for" (Set (Var "S")) "being"    ($#l2_incsp_1 :::"IncStruct"::: )    (Bool  "for" (Set (Var "F")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "the"  ($#u1_incsp_1 :::"Points"::: )  "of" (Set (Var "S"))) "holds"   (Bool  "("  (Bool (Set (Var "F")) "is"   ($#v4_incsp_1 :::"planar"::: )  ) "iff" (Bool  "ex" (Set (Var "P")) "being"   ($#m1_subset_1 :::"PLANE":::) "of" (Set (Var "S")) "st" (Bool (Set (Var "F"))  ($#r5_incsp_1 :::"on"::: )  (Set (Var "P"))))  ")" ))); 
 
theorem :: INCSP_1:1 (Bool  "for" (Set (Var "S")) "being"    ($#l1_incsp_1 :::"IncProjStr"::: )    (Bool  "for" (Set (Var "L")) "being"   ($#m1_subset_1 :::"LINE":::) "of" (Set (Var "S"))  (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "S")) "holds"   (Bool  "("  (Bool (Set  ($#k7_domain_1 :::"{"::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k7_domain_1 :::"}"::: ) )  ($#r4_incsp_1 :::"on"::: )  (Set (Var "L"))) "iff" (Bool  "("  (Bool (Set (Var "A"))  ($#r1_incsp_1 :::"on"::: )  (Set (Var "L"))) & (Bool (Set (Var "B"))  ($#r1_incsp_1 :::"on"::: )  (Set (Var "L")))  ")" )  ")" )))) ; 
 
theorem :: INCSP_1:2 (Bool  "for" (Set (Var "S")) "being"    ($#l1_incsp_1 :::"IncProjStr"::: )    (Bool  "for" (Set (Var "L")) "being"   ($#m1_subset_1 :::"LINE":::) "of" (Set (Var "S"))  (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being"   ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "S")) "holds"   (Bool  "("  (Bool (Set  ($#k8_domain_1 :::"{"::: ) (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) ($#k8_domain_1 :::"}"::: ) )  ($#r4_incsp_1 :::"on"::: )  (Set (Var "L"))) "iff" (Bool  "("  (Bool (Set (Var "A"))  ($#r1_incsp_1 :::"on"::: )  (Set (Var "L"))) & (Bool (Set (Var "B"))  ($#r1_incsp_1 :::"on"::: )  (Set (Var "L"))) & (Bool (Set (Var "C"))  ($#r1_incsp_1 :::"on"::: )  (Set (Var "L")))  ")" )  ")" )))) ; 
 
theorem :: INCSP_1:3 (Bool  "for" (Set (Var "S")) "being"    ($#l2_incsp_1 :::"IncStruct"::: )    (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "S"))  (Bool  "for" (Set (Var "P")) "being"   ($#m1_subset_1 :::"PLANE":::) "of" (Set (Var "S")) "holds"   (Bool  "("  (Bool (Set  ($#k7_domain_1 :::"{"::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k7_domain_1 :::"}"::: ) )  ($#r5_incsp_1 :::"on"::: )  (Set (Var "P"))) "iff" (Bool  "("  (Bool (Set (Var "A"))  ($#r2_incsp_1 :::"on"::: )  (Set (Var "P"))) & (Bool (Set (Var "B"))  ($#r2_incsp_1 :::"on"::: )  (Set (Var "P")))  ")" )  ")" )))) ; 
 
theorem :: INCSP_1:4 (Bool  "for" (Set (Var "S")) "being"    ($#l2_incsp_1 :::"IncStruct"::: )    (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being"   ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "S"))  (Bool  "for" (Set (Var "P")) "being"   ($#m1_subset_1 :::"PLANE":::) "of" (Set (Var "S")) "holds"   (Bool  "("  (Bool (Set  ($#k8_domain_1 :::"{"::: ) (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) ($#k8_domain_1 :::"}"::: ) )  ($#r5_incsp_1 :::"on"::: )  (Set (Var "P"))) "iff" (Bool  "("  (Bool (Set (Var "A"))  ($#r2_incsp_1 :::"on"::: )  (Set (Var "P"))) & (Bool (Set (Var "B"))  ($#r2_incsp_1 :::"on"::: )  (Set (Var "P"))) & (Bool (Set (Var "C"))  ($#r2_incsp_1 :::"on"::: )  (Set (Var "P")))  ")" )  ")" )))) ; 
 
theorem :: INCSP_1:5 (Bool  "for" (Set (Var "S")) "being"    ($#l2_incsp_1 :::"IncStruct"::: )    (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "," (Set (Var "D")) "being"   ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "S"))  (Bool  "for" (Set (Var "P")) "being"   ($#m1_subset_1 :::"PLANE":::) "of" (Set (Var "S")) "holds"   (Bool  "("  (Bool (Set  ($#k9_domain_1 :::"{"::: ) (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "," (Set (Var "D")) ($#k9_domain_1 :::"}"::: ) )  ($#r5_incsp_1 :::"on"::: )  (Set (Var "P"))) "iff" (Bool  "("  (Bool (Set (Var "A"))  ($#r2_incsp_1 :::"on"::: )  (Set (Var "P"))) & (Bool (Set (Var "B"))  ($#r2_incsp_1 :::"on"::: )  (Set (Var "P"))) & (Bool (Set (Var "C"))  ($#r2_incsp_1 :::"on"::: )  (Set (Var "P"))) & (Bool (Set (Var "D"))  ($#r2_incsp_1 :::"on"::: )  (Set (Var "P")))  ")" )  ")" )))) ; 
 
theorem :: INCSP_1:6 (Bool  "for" (Set (Var "S")) "being"    ($#l2_incsp_1 :::"IncStruct"::: )    (Bool  "for" (Set (Var "L")) "being"   ($#m1_subset_1 :::"LINE":::) "of" (Set (Var "S"))  (Bool  "for" (Set (Var "G")) "," (Set (Var "F")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "the"  ($#u1_incsp_1 :::"Points"::: )  "of" (Set (Var "S")))  "st" (Bool (Bool (Set (Var "G"))  ($#r1_tarski :::"c="::: )  (Set (Var "F"))) & (Bool (Set (Var "F"))  ($#r4_incsp_1 :::"on"::: )  (Set (Var "L")))) "holds"  (Bool (Set (Var "G"))  ($#r4_incsp_1 :::"on"::: )  (Set (Var "L")))))) ; 
 
theorem :: INCSP_1:7 (Bool  "for" (Set (Var "S")) "being"    ($#l2_incsp_1 :::"IncStruct"::: )    (Bool  "for" (Set (Var "P")) "being"   ($#m1_subset_1 :::"PLANE":::) "of" (Set (Var "S"))  (Bool  "for" (Set (Var "G")) "," (Set (Var "F")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "the"  ($#u1_incsp_1 :::"Points"::: )  "of" (Set (Var "S")))  "st" (Bool (Bool (Set (Var "G"))  ($#r1_tarski :::"c="::: )  (Set (Var "F"))) & (Bool (Set (Var "F"))  ($#r5_incsp_1 :::"on"::: )  (Set (Var "P")))) "holds"  (Bool (Set (Var "G"))  ($#r5_incsp_1 :::"on"::: )  (Set (Var "P")))))) ; 
 
theorem :: INCSP_1:8 (Bool  "for" (Set (Var "S")) "being"    ($#l2_incsp_1 :::"IncStruct"::: )    (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "S"))  (Bool  "for" (Set (Var "L")) "being"   ($#m1_subset_1 :::"LINE":::) "of" (Set (Var "S"))  (Bool  "for" (Set (Var "F")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "the"  ($#u1_incsp_1 :::"Points"::: )  "of" (Set (Var "S"))) "holds"   (Bool  "("  (Bool  "("  (Bool (Set (Var "F"))  ($#r4_incsp_1 :::"on"::: )  (Set (Var "L"))) & (Bool (Set (Var "A"))  ($#r1_incsp_1 :::"on"::: )  (Set (Var "L")))  ")" ) "iff" (Bool (Set (Set (Var "F"))  ($#k4_subset_1 :::"\/"::: )  (Set  ($#k6_domain_1 :::"{"::: ) (Set (Var "A")) ($#k6_domain_1 :::"}"::: ) ))  ($#r4_incsp_1 :::"on"::: )  (Set (Var "L")))  ")" ))))) ; 
 
theorem :: INCSP_1:9 (Bool  "for" (Set (Var "S")) "being"    ($#l2_incsp_1 :::"IncStruct"::: )    (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "S"))  (Bool  "for" (Set (Var "P")) "being"   ($#m1_subset_1 :::"PLANE":::) "of" (Set (Var "S"))  (Bool  "for" (Set (Var "F")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "the"  ($#u1_incsp_1 :::"Points"::: )  "of" (Set (Var "S"))) "holds"   (Bool  "("  (Bool  "("  (Bool (Set (Var "F"))  ($#r5_incsp_1 :::"on"::: )  (Set (Var "P"))) & (Bool (Set (Var "A"))  ($#r2_incsp_1 :::"on"::: )  (Set (Var "P")))  ")" ) "iff" (Bool (Set (Set (Var "F"))  ($#k4_subset_1 :::"\/"::: )  (Set  ($#k6_domain_1 :::"{"::: ) (Set (Var "A")) ($#k6_domain_1 :::"}"::: ) ))  ($#r5_incsp_1 :::"on"::: )  (Set (Var "P")))  ")" ))))) ; 
 
theorem :: INCSP_1:10 (Bool  "for" (Set (Var "S")) "being"    ($#l2_incsp_1 :::"IncStruct"::: )    (Bool  "for" (Set (Var "L")) "being"   ($#m1_subset_1 :::"LINE":::) "of" (Set (Var "S"))  (Bool  "for" (Set (Var "F")) "," (Set (Var "G")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "the"  ($#u1_incsp_1 :::"Points"::: )  "of" (Set (Var "S"))) "holds"   (Bool  "("  (Bool (Set (Set (Var "F"))  ($#k4_subset_1 :::"\/"::: )  (Set (Var "G")))  ($#r4_incsp_1 :::"on"::: )  (Set (Var "L"))) "iff" (Bool  "("  (Bool (Set (Var "F"))  ($#r4_incsp_1 :::"on"::: )  (Set (Var "L"))) & (Bool (Set (Var "G"))  ($#r4_incsp_1 :::"on"::: )  (Set (Var "L")))  ")" )  ")" )))) ; 
 
theorem :: INCSP_1:11 (Bool  "for" (Set (Var "S")) "being"    ($#l2_incsp_1 :::"IncStruct"::: )    (Bool  "for" (Set (Var "P")) "being"   ($#m1_subset_1 :::"PLANE":::) "of" (Set (Var "S"))  (Bool  "for" (Set (Var "F")) "," (Set (Var "G")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "the"  ($#u1_incsp_1 :::"Points"::: )  "of" (Set (Var "S"))) "holds"   (Bool  "("  (Bool (Set (Set (Var "F"))  ($#k4_subset_1 :::"\/"::: )  (Set (Var "G")))  ($#r5_incsp_1 :::"on"::: )  (Set (Var "P"))) "iff" (Bool  "("  (Bool (Set (Var "F"))  ($#r5_incsp_1 :::"on"::: )  (Set (Var "P"))) & (Bool (Set (Var "G"))  ($#r5_incsp_1 :::"on"::: )  (Set (Var "P")))  ")" )  ")" )))) ; 
 
theorem :: INCSP_1:12 (Bool  "for" (Set (Var "S")) "being"    ($#l2_incsp_1 :::"IncStruct"::: )    (Bool  "for" (Set (Var "G")) "," (Set (Var "F")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "the"  ($#u1_incsp_1 :::"Points"::: )  "of" (Set (Var "S")))  "st" (Bool (Bool (Set (Var "G"))  ($#r1_tarski :::"c="::: )  (Set (Var "F"))) & (Bool (Set (Var "F")) "is"   ($#v3_incsp_1 :::"linear"::: )  )) "holds"  (Bool (Set (Var "G")) "is"   ($#v3_incsp_1 :::"linear"::: )  ))) ; 
 
theorem :: INCSP_1:13 (Bool  "for" (Set (Var "S")) "being"    ($#l2_incsp_1 :::"IncStruct"::: )    (Bool  "for" (Set (Var "G")) "," (Set (Var "F")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "the"  ($#u1_incsp_1 :::"Points"::: )  "of" (Set (Var "S")))  "st" (Bool (Bool (Set (Var "G"))  ($#r1_tarski :::"c="::: )  (Set (Var "F"))) & (Bool (Set (Var "F")) "is"   ($#v4_incsp_1 :::"planar"::: )  )) "holds"  (Bool (Set (Var "G")) "is"   ($#v4_incsp_1 :::"planar"::: )  ))) ; 
 definitionlet "S" be    ($#l1_incsp_1 :::"IncProjStr"::: )  ; attr "S" is  :::"with_non-trivial_lines":::  means :: INCSP_1:def 8 (Bool  "for" (Set (Var "L")) "being"   ($#m1_subset_1 :::"LINE":::) "of" "S" (Bool  "ex" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#m1_subset_1 :::"POINT":::) "of" "S" "st"  (Bool  "("  (Bool (Set (Var "A"))  ($#r1_hidden :::"<>"::: )  (Set (Var "B"))) & (Bool (Set  ($#k7_domain_1 :::"{"::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k7_domain_1 :::"}"::: ) )  ($#r4_incsp_1 :::"on"::: )  (Set (Var "L")))  ")" ))); attr "S" is  :::"linear":::  means :: INCSP_1:def 9 (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#m1_subset_1 :::"POINT":::) "of" "S" (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"))))); attr "S" is  :::"up-2-rank":::  means :: INCSP_1:def 10 (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#m1_subset_1 :::"POINT":::) "of" "S"  (Bool  "for" (Set (Var "K")) "," (Set (Var "L")) "being"   ($#m1_subset_1 :::"LINE":::) "of" "S"  "st" (Bool (Bool (Set (Var "A"))  ($#r1_hidden :::"<>"::: )  (Set (Var "B"))) & (Bool (Set  ($#k7_domain_1 :::"{"::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k7_domain_1 :::"}"::: ) )  ($#r4_incsp_1 :::"on"::: )  (Set (Var "K"))) & (Bool (Set  ($#k7_domain_1 :::"{"::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k7_domain_1 :::"}"::: ) )  ($#r4_incsp_1 :::"on"::: )  (Set (Var "L")))) "holds"  (Bool (Set (Var "K"))  ($#r1_hidden :::"="::: )  (Set (Var "L"))))); end; 












:: deftheorem    defines :::"with_non-trivial_lines"::: INCSP_1:def 8 :  (Bool  "for" (Set (Var "S")) "being"    ($#l1_incsp_1 :::"IncProjStr"::: )   "holds"   (Bool  "("  (Bool (Set (Var "S")) "is"   ($#v5_incsp_1 :::"with_non-trivial_lines"::: )  ) "iff" (Bool  "for" (Set (Var "L")) "being"   ($#m1_subset_1 :::"LINE":::) "of" (Set (Var "S")) (Bool  "ex" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "S")) "st"  (Bool  "("  (Bool (Set (Var "A"))  ($#r1_hidden :::"<>"::: )  (Set (Var "B"))) & (Bool (Set  ($#k7_domain_1 :::"{"::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k7_domain_1 :::"}"::: ) )  ($#r4_incsp_1 :::"on"::: )  (Set (Var "L")))  ")" )))  ")" )); 
 
:: deftheorem    defines :::"linear"::: INCSP_1:def 9 :  (Bool  "for" (Set (Var "S")) "being"    ($#l1_incsp_1 :::"IncProjStr"::: )   "holds"   (Bool  "("  (Bool (Set (Var "S")) "is"   ($#v6_incsp_1 :::"linear"::: )  ) "iff" (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "S")) (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")))))  ")" )); 
 
:: deftheorem    defines :::"up-2-rank"::: INCSP_1:def 10 :  (Bool  "for" (Set (Var "S")) "being"    ($#l1_incsp_1 :::"IncProjStr"::: )   "holds"   (Bool  "("  (Bool (Set (Var "S")) "is"   ($#v7_incsp_1 :::"up-2-rank"::: )  ) "iff" (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "S"))  (Bool  "for" (Set (Var "K")) "," (Set (Var "L")) "being"   ($#m1_subset_1 :::"LINE":::) "of" (Set (Var "S"))  "st" (Bool (Bool (Set (Var "A"))  ($#r1_hidden :::"<>"::: )  (Set (Var "B"))) & (Bool (Set  ($#k7_domain_1 :::"{"::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k7_domain_1 :::"}"::: ) )  ($#r4_incsp_1 :::"on"::: )  (Set (Var "K"))) & (Bool (Set  ($#k7_domain_1 :::"{"::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k7_domain_1 :::"}"::: ) )  ($#r4_incsp_1 :::"on"::: )  (Set (Var "L")))) "holds"  (Bool (Set (Var "K"))  ($#r1_hidden :::"="::: )  (Set (Var "L")))))  ")" )); 
 definitionlet "S" be    ($#l2_incsp_1 :::"IncStruct"::: )  ; attr "S" is  :::"with_non-empty_planes":::  means :: INCSP_1:def 11 (Bool  "for" (Set (Var "P")) "being"   ($#m1_subset_1 :::"PLANE":::) "of" "S" (Bool  "ex" (Set (Var "A")) "being"   ($#m1_subset_1 :::"POINT":::) "of" "S" "st" (Bool (Set (Var "A"))  ($#r2_incsp_1 :::"on"::: )  (Set (Var "P"))))); attr "S" is  :::"planar":::  means :: INCSP_1:def 12 (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being"   ($#m1_subset_1 :::"POINT":::) "of" "S" (Bool  "ex" (Set (Var "P")) "being"   ($#m1_subset_1 :::"PLANE":::) "of" "S" "st" (Bool (Set  ($#k8_domain_1 :::"{"::: ) (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) ($#k8_domain_1 :::"}"::: ) )  ($#r5_incsp_1 :::"on"::: )  (Set (Var "P"))))); attr "S" is  :::"with_<=1_plane_per_3_pts":::  means :: INCSP_1:def 13 (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being"   ($#m1_subset_1 :::"POINT":::) "of" "S"  (Bool  "for" (Set (Var "P")) "," (Set (Var "Q")) "being"   ($#m1_subset_1 :::"PLANE":::) "of" "S"  "st" (Bool (Bool (Bool  "not" (Set  ($#k8_domain_1 :::"{"::: ) (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) ($#k8_domain_1 :::"}"::: ) ) "is"   ($#v3_incsp_1 :::"linear"::: )  )) & (Bool (Set  ($#k8_domain_1 :::"{"::: ) (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) ($#k8_domain_1 :::"}"::: ) )  ($#r5_incsp_1 :::"on"::: )  (Set (Var "P"))) & (Bool (Set  ($#k8_domain_1 :::"{"::: ) (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) ($#k8_domain_1 :::"}"::: ) )  ($#r5_incsp_1 :::"on"::: )  (Set (Var "Q")))) "holds"  (Bool (Set (Var "P"))  ($#r1_hidden :::"="::: )  (Set (Var "Q"))))); attr "S" is  :::"with_lines_inside_planes":::  means :: INCSP_1:def 14 (Bool  "for" (Set (Var "L")) "being"   ($#m1_subset_1 :::"LINE":::) "of" "S"  (Bool  "for" (Set (Var "P")) "being"   ($#m1_subset_1 :::"PLANE":::) "of" "S"  "st" (Bool (Bool  "ex" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#m1_subset_1 :::"POINT":::) "of" "S" "st"  (Bool  "("  (Bool (Set (Var "A"))  ($#r1_hidden :::"<>"::: )  (Set (Var "B"))) & (Bool (Set  ($#k7_domain_1 :::"{"::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k7_domain_1 :::"}"::: ) )  ($#r4_incsp_1 :::"on"::: )  (Set (Var "L"))) & (Bool (Set  ($#k7_domain_1 :::"{"::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k7_domain_1 :::"}"::: ) )  ($#r5_incsp_1 :::"on"::: )  (Set (Var "P")))  ")" ))) "holds"  (Bool (Set (Var "L"))  ($#r3_incsp_1 :::"on"::: )  (Set (Var "P"))))); attr "S" is  :::"with_planes_intersecting_in_2_pts":::  means :: INCSP_1:def 15 (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"POINT":::) "of" "S"  (Bool  "for" (Set (Var "P")) "," (Set (Var "Q")) "being"   ($#m1_subset_1 :::"PLANE":::) "of" "S"  "st" (Bool (Bool (Set (Var "A"))  ($#r2_incsp_1 :::"on"::: )  (Set (Var "P"))) & (Bool (Set (Var "A"))  ($#r2_incsp_1 :::"on"::: )  (Set (Var "Q")))) "holds"  (Bool  "ex" (Set (Var "B")) "being"   ($#m1_subset_1 :::"POINT":::) "of" "S" "st"  (Bool  "("  (Bool (Set (Var "A"))  ($#r1_hidden :::"<>"::: )  (Set (Var "B"))) & (Bool (Set (Var "B"))  ($#r2_incsp_1 :::"on"::: )  (Set (Var "P"))) & (Bool (Set (Var "B"))  ($#r2_incsp_1 :::"on"::: )  (Set (Var "Q")))  ")" )))); attr "S" is  :::"up-3-dimensional":::  means :: INCSP_1:def 16 (Bool  "not" (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "," (Set (Var "D")) "being"   ($#m1_subset_1 :::"POINT":::) "of" "S" "holds"  (Bool (Set  ($#k9_domain_1 :::"{"::: ) (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "," (Set (Var "D")) ($#k9_domain_1 :::"}"::: ) ) "is"   ($#v4_incsp_1 :::"planar"::: )  ))); attr "S" is  :::"inc-compatible":::  means :: INCSP_1:def 17 (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"POINT":::) "of" "S"  (Bool  "for" (Set (Var "L")) "being"   ($#m1_subset_1 :::"LINE":::) "of" "S"  (Bool  "for" (Set (Var "P")) "being"   ($#m1_subset_1 :::"PLANE":::) "of" "S"  "st" (Bool (Bool (Set (Var "A"))  ($#r1_incsp_1 :::"on"::: )  (Set (Var "L"))) & (Bool (Set (Var "L"))  ($#r3_incsp_1 :::"on"::: )  (Set (Var "P")))) "holds"  (Bool (Set (Var "A"))  ($#r2_incsp_1 :::"on"::: )  (Set (Var "P")))))); end; 




























:: deftheorem    defines :::"with_non-empty_planes"::: INCSP_1:def 11 :  (Bool  "for" (Set (Var "S")) "being"    ($#l2_incsp_1 :::"IncStruct"::: )   "holds"   (Bool  "("  (Bool (Set (Var "S")) "is"   ($#v8_incsp_1 :::"with_non-empty_planes"::: )  ) "iff" (Bool  "for" (Set (Var "P")) "being"   ($#m1_subset_1 :::"PLANE":::) "of" (Set (Var "S")) (Bool  "ex" (Set (Var "A")) "being"   ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "S")) "st" (Bool (Set (Var "A"))  ($#r2_incsp_1 :::"on"::: )  (Set (Var "P")))))  ")" )); 
 
:: deftheorem    defines :::"planar"::: INCSP_1:def 12 :  (Bool  "for" (Set (Var "S")) "being"    ($#l2_incsp_1 :::"IncStruct"::: )   "holds"   (Bool  "("  (Bool (Set (Var "S")) "is"   ($#v9_incsp_1 :::"planar"::: )  ) "iff" (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being"   ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "S")) (Bool  "ex" (Set (Var "P")) "being"   ($#m1_subset_1 :::"PLANE":::) "of" (Set (Var "S")) "st" (Bool (Set  ($#k8_domain_1 :::"{"::: ) (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) ($#k8_domain_1 :::"}"::: ) )  ($#r5_incsp_1 :::"on"::: )  (Set (Var "P")))))  ")" )); 
 
:: deftheorem    defines :::"with_<=1_plane_per_3_pts"::: INCSP_1:def 13 :  (Bool  "for" (Set (Var "S")) "being"    ($#l2_incsp_1 :::"IncStruct"::: )   "holds"   (Bool  "("  (Bool (Set (Var "S")) "is"   ($#v10_incsp_1 :::"with_<=1_plane_per_3_pts"::: )  ) "iff" (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being"   ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "S"))  (Bool  "for" (Set (Var "P")) "," (Set (Var "Q")) "being"   ($#m1_subset_1 :::"PLANE":::) "of" (Set (Var "S"))  "st" (Bool (Bool (Bool  "not" (Set  ($#k8_domain_1 :::"{"::: ) (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) ($#k8_domain_1 :::"}"::: ) ) "is"   ($#v3_incsp_1 :::"linear"::: )  )) & (Bool (Set  ($#k8_domain_1 :::"{"::: ) (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) ($#k8_domain_1 :::"}"::: ) )  ($#r5_incsp_1 :::"on"::: )  (Set (Var "P"))) & (Bool (Set  ($#k8_domain_1 :::"{"::: ) (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) ($#k8_domain_1 :::"}"::: ) )  ($#r5_incsp_1 :::"on"::: )  (Set (Var "Q")))) "holds"  (Bool (Set (Var "P"))  ($#r1_hidden :::"="::: )  (Set (Var "Q")))))  ")" )); 
 
:: deftheorem    defines :::"with_lines_inside_planes"::: INCSP_1:def 14 :  (Bool  "for" (Set (Var "S")) "being"    ($#l2_incsp_1 :::"IncStruct"::: )   "holds"   (Bool  "("  (Bool (Set (Var "S")) "is"   ($#v11_incsp_1 :::"with_lines_inside_planes"::: )  ) "iff" (Bool  "for" (Set (Var "L")) "being"   ($#m1_subset_1 :::"LINE":::) "of" (Set (Var "S"))  (Bool  "for" (Set (Var "P")) "being"   ($#m1_subset_1 :::"PLANE":::) "of" (Set (Var "S"))  "st" (Bool (Bool  "ex" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "S")) "st"  (Bool  "("  (Bool (Set (Var "A"))  ($#r1_hidden :::"<>"::: )  (Set (Var "B"))) & (Bool (Set  ($#k7_domain_1 :::"{"::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k7_domain_1 :::"}"::: ) )  ($#r4_incsp_1 :::"on"::: )  (Set (Var "L"))) & (Bool (Set  ($#k7_domain_1 :::"{"::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k7_domain_1 :::"}"::: ) )  ($#r5_incsp_1 :::"on"::: )  (Set (Var "P")))  ")" ))) "holds"  (Bool (Set (Var "L"))  ($#r3_incsp_1 :::"on"::: )  (Set (Var "P")))))  ")" )); 
 
:: deftheorem    defines :::"with_planes_intersecting_in_2_pts"::: INCSP_1:def 15 :  (Bool  "for" (Set (Var "S")) "being"    ($#l2_incsp_1 :::"IncStruct"::: )   "holds"   (Bool  "("  (Bool (Set (Var "S")) "is"   ($#v12_incsp_1 :::"with_planes_intersecting_in_2_pts"::: )  ) "iff" (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "S"))  (Bool  "for" (Set (Var "P")) "," (Set (Var "Q")) "being"   ($#m1_subset_1 :::"PLANE":::) "of" (Set (Var "S"))  "st" (Bool (Bool (Set (Var "A"))  ($#r2_incsp_1 :::"on"::: )  (Set (Var "P"))) & (Bool (Set (Var "A"))  ($#r2_incsp_1 :::"on"::: )  (Set (Var "Q")))) "holds"  (Bool  "ex" (Set (Var "B")) "being"   ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "S")) "st"  (Bool  "("  (Bool (Set (Var "A"))  ($#r1_hidden :::"<>"::: )  (Set (Var "B"))) & (Bool (Set (Var "B"))  ($#r2_incsp_1 :::"on"::: )  (Set (Var "P"))) & (Bool (Set (Var "B"))  ($#r2_incsp_1 :::"on"::: )  (Set (Var "Q")))  ")" ))))  ")" )); 
 
:: deftheorem    defines :::"up-3-dimensional"::: INCSP_1:def 16 :  (Bool  "for" (Set (Var "S")) "being"    ($#l2_incsp_1 :::"IncStruct"::: )   "holds"   (Bool  "("  (Bool (Set (Var "S")) "is"   ($#v13_incsp_1 :::"up-3-dimensional"::: )  ) "iff" (Bool  "not" (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "," (Set (Var "D")) "being"   ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "S")) "holds"  (Bool (Set  ($#k9_domain_1 :::"{"::: ) (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "," (Set (Var "D")) ($#k9_domain_1 :::"}"::: ) ) "is"   ($#v4_incsp_1 :::"planar"::: )  )))  ")" )); 
 
:: deftheorem    defines :::"inc-compatible"::: INCSP_1:def 17 :  (Bool  "for" (Set (Var "S")) "being"    ($#l2_incsp_1 :::"IncStruct"::: )   "holds"   (Bool  "("  (Bool (Set (Var "S")) "is"   ($#v14_incsp_1 :::"inc-compatible"::: )  ) "iff" (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "S"))  (Bool  "for" (Set (Var "L")) "being"   ($#m1_subset_1 :::"LINE":::) "of" (Set (Var "S"))  (Bool  "for" (Set (Var "P")) "being"   ($#m1_subset_1 :::"PLANE":::) "of" (Set (Var "S"))  "st" (Bool (Bool (Set (Var "A"))  ($#r1_incsp_1 :::"on"::: )  (Set (Var "L"))) & (Bool (Set (Var "L"))  ($#r3_incsp_1 :::"on"::: )  (Set (Var "P")))) "holds"  (Bool (Set (Var "A"))  ($#r2_incsp_1 :::"on"::: )  (Set (Var "P"))))))  ")" )); 
 definitionlet "IT" be    ($#l2_incsp_1 :::"IncStruct"::: )  ; attr "IT" is  :::"IncSpace-like":::  means :: INCSP_1:def 18 (Bool  "("  (Bool "IT" "is"   ($#v5_incsp_1 :::"with_non-trivial_lines"::: )  ) & (Bool "IT" "is"   ($#v6_incsp_1 :::"linear"::: )  ) & (Bool "IT" "is"   ($#v7_incsp_1 :::"up-2-rank"::: )  ) & (Bool "IT" "is"   ($#v8_incsp_1 :::"with_non-empty_planes"::: )  ) & (Bool "IT" "is"   ($#v9_incsp_1 :::"planar"::: )  ) & (Bool "IT" "is"   ($#v10_incsp_1 :::"with_<=1_plane_per_3_pts"::: )  ) & (Bool "IT" "is"   ($#v11_incsp_1 :::"with_lines_inside_planes"::: )  ) & (Bool "IT" "is"   ($#v12_incsp_1 :::"with_planes_intersecting_in_2_pts"::: )  ) & (Bool "IT" "is"   ($#v13_incsp_1 :::"up-3-dimensional"::: )  ) & (Bool "IT" "is"   ($#v14_incsp_1 :::"inc-compatible"::: )  )  ")" ); end; 




:: deftheorem    defines :::"IncSpace-like"::: INCSP_1:def 18 :  (Bool  "for" (Set (Var "IT")) "being"    ($#l2_incsp_1 :::"IncStruct"::: )   "holds"   (Bool  "("  (Bool (Set (Var "IT")) "is"   ($#v15_incsp_1 :::"IncSpace-like"::: )  ) "iff" (Bool  "("  (Bool (Set (Var "IT")) "is"   ($#v5_incsp_1 :::"with_non-trivial_lines"::: )  ) & (Bool (Set (Var "IT")) "is"   ($#v6_incsp_1 :::"linear"::: )  ) & (Bool (Set (Var "IT")) "is"   ($#v7_incsp_1 :::"up-2-rank"::: )  ) & (Bool (Set (Var "IT")) "is"   ($#v8_incsp_1 :::"with_non-empty_planes"::: )  ) & (Bool (Set (Var "IT")) "is"   ($#v9_incsp_1 :::"planar"::: )  ) & (Bool (Set (Var "IT")) "is"   ($#v10_incsp_1 :::"with_<=1_plane_per_3_pts"::: )  ) & (Bool (Set (Var "IT")) "is"   ($#v11_incsp_1 :::"with_lines_inside_planes"::: )  ) & (Bool (Set (Var "IT")) "is"   ($#v12_incsp_1 :::"with_planes_intersecting_in_2_pts"::: )  ) & (Bool (Set (Var "IT")) "is"   ($#v13_incsp_1 :::"up-3-dimensional"::: )  ) & (Bool (Set (Var "IT")) "is"   ($#v14_incsp_1 :::"inc-compatible"::: )  )  ")" )  ")" )); 
 




registration
cluster   ($#v15_incsp_1 :::"IncSpace-like"::: )    ->   ($#v5_incsp_1 :::"with_non-trivial_lines"::: )     ($#v6_incsp_1 :::"linear"::: )     ($#v7_incsp_1 :::"up-2-rank"::: )     ($#v8_incsp_1 :::"with_non-empty_planes"::: )     ($#v9_incsp_1 :::"planar"::: )     ($#v10_incsp_1 :::"with_<=1_plane_per_3_pts"::: )     ($#v11_incsp_1 :::"with_lines_inside_planes"::: )     ($#v12_incsp_1 :::"with_planes_intersecting_in_2_pts"::: )     ($#v13_incsp_1 :::"up-3-dimensional"::: )     ($#v14_incsp_1 :::"inc-compatible"::: )    for    ($#l2_incsp_1 :::"IncStruct"::: )  ; 
end; registration
cluster   ($#v2_incsp_1 :::"strict"::: )     ($#v15_incsp_1 :::"IncSpace-like"::: )    for    ($#l2_incsp_1 :::"IncStruct"::: )  ; 
end; definitionmode IncSpace is   ($#v15_incsp_1 :::"IncSpace-like"::: )     ($#l2_incsp_1 :::"IncStruct"::: )  ; end; 

























theorem :: INCSP_1:14 (Bool  "for" (Set (Var "S")) "being"   ($#l2_incsp_1 :::"IncSpace":::)  (Bool  "for" (Set (Var "L")) "being"   ($#m1_subset_1 :::"LINE":::) "of" (Set (Var "S"))  (Bool  "for" (Set (Var "P")) "being"   ($#m1_subset_1 :::"PLANE":::) "of" (Set (Var "S"))  (Bool  "for" (Set (Var "F")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "the"  ($#u1_incsp_1 :::"Points"::: )  "of" (Set (Var "S")))  "st" (Bool (Bool (Set (Var "F"))  ($#r4_incsp_1 :::"on"::: )  (Set (Var "L"))) & (Bool (Set (Var "L"))  ($#r3_incsp_1 :::"on"::: )  (Set (Var "P")))) "holds"  (Bool (Set (Var "F"))  ($#r5_incsp_1 :::"on"::: )  (Set (Var "P"))))))) ; 
 
theorem :: INCSP_1:15 (Bool  "for" (Set (Var "S")) "being"   ($#l2_incsp_1 :::"IncSpace":::)  (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "S")) "holds"  (Bool (Set  ($#k8_domain_1 :::"{"::: ) (Set (Var "A")) "," (Set (Var "A")) "," (Set (Var "B")) ($#k8_domain_1 :::"}"::: ) ) "is"   ($#v3_incsp_1 :::"linear"::: )  ))) ; 
 
theorem :: INCSP_1:16 (Bool  "for" (Set (Var "S")) "being"   ($#l2_incsp_1 :::"IncSpace":::)  (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being"   ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "S")) "holds"  (Bool (Set  ($#k9_domain_1 :::"{"::: ) (Set (Var "A")) "," (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) ($#k9_domain_1 :::"}"::: ) ) "is"   ($#v4_incsp_1 :::"planar"::: )  ))) ; 
 
theorem :: INCSP_1:17 (Bool  "for" (Set (Var "S")) "being"   ($#l2_incsp_1 :::"IncSpace":::)  (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "," (Set (Var "D")) "being"   ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "S"))  "st" (Bool (Bool (Set  ($#k8_domain_1 :::"{"::: ) (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) ($#k8_domain_1 :::"}"::: ) ) "is"   ($#v3_incsp_1 :::"linear"::: )  )) "holds"  (Bool (Set  ($#k9_domain_1 :::"{"::: ) (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "," (Set (Var "D")) ($#k9_domain_1 :::"}"::: ) ) "is"   ($#v4_incsp_1 :::"planar"::: )  ))) ; 
 
theorem :: INCSP_1:18 (Bool  "for" (Set (Var "S")) "being"   ($#l2_incsp_1 :::"IncSpace":::)  (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being"   ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "S"))  (Bool  "for" (Set (Var "L")) "being"   ($#m1_subset_1 :::"LINE":::) "of" (Set (Var "S"))  "st" (Bool (Bool (Set (Var "A"))  ($#r1_hidden :::"<>"::: )  (Set (Var "B"))) & (Bool (Set  ($#k7_domain_1 :::"{"::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k7_domain_1 :::"}"::: ) )  ($#r4_incsp_1 :::"on"::: )  (Set (Var "L"))) & (Bool (Bool  "not" (Set (Var "C"))  ($#r1_incsp_1 :::"on"::: )  (Set (Var "L"))))) "holds"  (Bool  "not" (Bool (Set  ($#k8_domain_1 :::"{"::: ) (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) ($#k8_domain_1 :::"}"::: ) ) "is"   ($#v3_incsp_1 :::"linear"::: )  ))))) ; 
 
theorem :: INCSP_1:19 (Bool  "for" (Set (Var "S")) "being"   ($#l2_incsp_1 :::"IncSpace":::)  (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "," (Set (Var "D")) "being"   ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "S"))  (Bool  "for" (Set (Var "P")) "being"   ($#m1_subset_1 :::"PLANE":::) "of" (Set (Var "S"))  "st" (Bool (Bool (Bool  "not" (Set  ($#k8_domain_1 :::"{"::: ) (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) ($#k8_domain_1 :::"}"::: ) ) "is"   ($#v3_incsp_1 :::"linear"::: )  )) & (Bool (Set  ($#k8_domain_1 :::"{"::: ) (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) ($#k8_domain_1 :::"}"::: ) )  ($#r5_incsp_1 :::"on"::: )  (Set (Var "P"))) & (Bool (Bool  "not" (Set (Var "D"))  ($#r2_incsp_1 :::"on"::: )  (Set (Var "P"))))) "holds"  (Bool  "not" (Bool (Set  ($#k9_domain_1 :::"{"::: ) (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "," (Set (Var "D")) ($#k9_domain_1 :::"}"::: ) ) "is"   ($#v4_incsp_1 :::"planar"::: )  ))))) ; 
 
theorem :: INCSP_1:20 (Bool  "for" (Set (Var "S")) "being"   ($#l2_incsp_1 :::"IncSpace":::)  (Bool  "for" (Set (Var "K")) "," (Set (Var "L")) "being"   ($#m1_subset_1 :::"LINE":::) "of" (Set (Var "S"))  "st" (Bool (Bool  "("   "for" (Set (Var "P")) "being"   ($#m1_subset_1 :::"PLANE":::) "of" (Set (Var "S"))  "holds"  (Bool  "("   "not" (Bool (Set (Var "K"))  ($#r3_incsp_1 :::"on"::: )  (Set (Var "P"))) "or"  "not" (Bool (Set (Var "L"))  ($#r3_incsp_1 :::"on"::: )  (Set (Var "P")))  ")" )  ")" )) "holds"  (Bool (Set (Var "K"))  ($#r1_hidden :::"<>"::: )  (Set (Var "L"))))) ; 
 
theorem :: INCSP_1:21 (Bool  "for" (Set (Var "S")) "being"   ($#l2_incsp_1 :::"IncSpace":::)  (Bool  "for" (Set (Var "L")) "," (Set (Var "L1")) "," (Set (Var "L2")) "being"   ($#m1_subset_1 :::"LINE":::) "of" (Set (Var "S"))  "st" (Bool (Bool  "("   "for" (Set (Var "P")) "being"   ($#m1_subset_1 :::"PLANE":::) "of" (Set (Var "S"))  "holds"  (Bool  "("   "not" (Bool (Set (Var "L"))  ($#r3_incsp_1 :::"on"::: )  (Set (Var "P"))) "or"  "not" (Bool (Set (Var "L1"))  ($#r3_incsp_1 :::"on"::: )  (Set (Var "P"))) "or"  "not" (Bool (Set (Var "L2"))  ($#r3_incsp_1 :::"on"::: )  (Set (Var "P")))  ")" )  ")" ) & (Bool  "ex" (Set (Var "A")) "being"   ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "S")) "st"  (Bool  "("  (Bool (Set (Var "A"))  ($#r1_incsp_1 :::"on"::: )  (Set (Var "L"))) & (Bool (Set (Var "A"))  ($#r1_incsp_1 :::"on"::: )  (Set (Var "L1"))) & (Bool (Set (Var "A"))  ($#r1_incsp_1 :::"on"::: )  (Set (Var "L2")))  ")" ))) "holds"  (Bool (Set (Var "L"))  ($#r1_hidden :::"<>"::: )  (Set (Var "L1"))))) ; 
 
theorem :: INCSP_1:22 (Bool  "for" (Set (Var "S")) "being"   ($#l2_incsp_1 :::"IncSpace":::)  (Bool  "for" (Set (Var "L1")) "," (Set (Var "L2")) "," (Set (Var "L")) "being"   ($#m1_subset_1 :::"LINE":::) "of" (Set (Var "S"))  (Bool  "for" (Set (Var "P")) "being"   ($#m1_subset_1 :::"PLANE":::) "of" (Set (Var "S"))  "st" (Bool (Bool (Set (Var "L1"))  ($#r3_incsp_1 :::"on"::: )  (Set (Var "P"))) & (Bool (Set (Var "L2"))  ($#r3_incsp_1 :::"on"::: )  (Set (Var "P"))) & (Bool (Bool  "not" (Set (Var "L"))  ($#r3_incsp_1 :::"on"::: )  (Set (Var "P")))) & (Bool (Set (Var "L1"))  ($#r1_hidden :::"<>"::: )  (Set (Var "L2")))) "holds"  (Bool  "for" (Set (Var "Q")) "being"   ($#m1_subset_1 :::"PLANE":::) "of" (Set (Var "S"))  "holds"  (Bool  "("   "not" (Bool (Set (Var "L"))  ($#r3_incsp_1 :::"on"::: )  (Set (Var "Q"))) "or"  "not" (Bool (Set (Var "L1"))  ($#r3_incsp_1 :::"on"::: )  (Set (Var "Q"))) "or"  "not" (Bool (Set (Var "L2"))  ($#r3_incsp_1 :::"on"::: )  (Set (Var "Q")))  ")" ))))) ; 
 
theorem :: INCSP_1:23 (Bool  "for" (Set (Var "S")) "being"   ($#l2_incsp_1 :::"IncSpace":::)  (Bool  "for" (Set (Var "K")) "," (Set (Var "L")) "being"   ($#m1_subset_1 :::"LINE":::) "of" (Set (Var "S"))  "st" (Bool (Bool  "ex" (Set (Var "A")) "being"   ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "S")) "st"  (Bool  "("  (Bool (Set (Var "A"))  ($#r1_incsp_1 :::"on"::: )  (Set (Var "K"))) & (Bool (Set (Var "A"))  ($#r1_incsp_1 :::"on"::: )  (Set (Var "L")))  ")" ))) "holds"  (Bool  "ex" (Set (Var "P")) "being"   ($#m1_subset_1 :::"PLANE":::) "of" (Set (Var "S")) "st"  (Bool  "("  (Bool (Set (Var "K"))  ($#r3_incsp_1 :::"on"::: )  (Set (Var "P"))) & (Bool (Set (Var "L"))  ($#r3_incsp_1 :::"on"::: )  (Set (Var "P")))  ")" )))) ; 
 
theorem :: INCSP_1:24 (Bool  "for" (Set (Var "S")) "being"   ($#l2_incsp_1 :::"IncSpace":::)  (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "S"))  "st" (Bool (Bool (Set (Var "A"))  ($#r1_hidden :::"<>"::: )  (Set (Var "B")))) "holds"  (Bool  "ex" (Set (Var "L")) "being"   ($#m1_subset_1 :::"LINE":::) "of" (Set (Var "S")) "st"  (Bool  "for" (Set (Var "K")) "being"   ($#m1_subset_1 :::"LINE":::) "of" (Set (Var "S")) "holds"   (Bool  "("  (Bool (Set  ($#k7_domain_1 :::"{"::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k7_domain_1 :::"}"::: ) )  ($#r4_incsp_1 :::"on"::: )  (Set (Var "K"))) "iff" (Bool (Set (Var "K"))  ($#r1_hidden :::"="::: )  (Set (Var "L")))  ")" ))))) ; 
 
theorem :: INCSP_1:25 (Bool  "for" (Set (Var "S")) "being"   ($#l2_incsp_1 :::"IncSpace":::)  (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being"   ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "S"))  "st" (Bool (Bool (Bool  "not" (Set  ($#k8_domain_1 :::"{"::: ) (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) ($#k8_domain_1 :::"}"::: ) ) "is"   ($#v3_incsp_1 :::"linear"::: )  ))) "holds"  (Bool  "ex" (Set (Var "P")) "being"   ($#m1_subset_1 :::"PLANE":::) "of" (Set (Var "S")) "st"  (Bool  "for" (Set (Var "Q")) "being"   ($#m1_subset_1 :::"PLANE":::) "of" (Set (Var "S")) "holds"   (Bool  "("  (Bool (Set  ($#k8_domain_1 :::"{"::: ) (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) ($#k8_domain_1 :::"}"::: ) )  ($#r5_incsp_1 :::"on"::: )  (Set (Var "Q"))) "iff" (Bool (Set (Var "P"))  ($#r1_hidden :::"="::: )  (Set (Var "Q")))  ")" ))))) ; 
 
theorem :: INCSP_1:26 (Bool  "for" (Set (Var "S")) "being"   ($#l2_incsp_1 :::"IncSpace":::)  (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "S"))  (Bool  "for" (Set (Var "L")) "being"   ($#m1_subset_1 :::"LINE":::) "of" (Set (Var "S"))  "st" (Bool (Bool (Bool  "not" (Set (Var "A"))  ($#r1_incsp_1 :::"on"::: )  (Set (Var "L"))))) "holds"  (Bool  "ex" (Set (Var "P")) "being"   ($#m1_subset_1 :::"PLANE":::) "of" (Set (Var "S")) "st"  (Bool  "for" (Set (Var "Q")) "being"   ($#m1_subset_1 :::"PLANE":::) "of" (Set (Var "S")) "holds"   (Bool  "("  (Bool  "("  (Bool (Set (Var "A"))  ($#r2_incsp_1 :::"on"::: )  (Set (Var "Q"))) & (Bool (Set (Var "L"))  ($#r3_incsp_1 :::"on"::: )  (Set (Var "Q")))  ")" ) "iff" (Bool (Set (Var "P"))  ($#r1_hidden :::"="::: )  (Set (Var "Q")))  ")" )))))) ; 
 
theorem :: INCSP_1:27 (Bool  "for" (Set (Var "S")) "being"   ($#l2_incsp_1 :::"IncSpace":::)  (Bool  "for" (Set (Var "K")) "," (Set (Var "L")) "being"   ($#m1_subset_1 :::"LINE":::) "of" (Set (Var "S"))  "st" (Bool (Bool (Set (Var "K"))  ($#r1_hidden :::"<>"::: )  (Set (Var "L"))) & (Bool  "ex" (Set (Var "A")) "being"   ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "S")) "st"  (Bool  "("  (Bool (Set (Var "A"))  ($#r1_incsp_1 :::"on"::: )  (Set (Var "K"))) & (Bool (Set (Var "A"))  ($#r1_incsp_1 :::"on"::: )  (Set (Var "L")))  ")" ))) "holds"  (Bool  "ex" (Set (Var "P")) "being"   ($#m1_subset_1 :::"PLANE":::) "of" (Set (Var "S")) "st"  (Bool  "for" (Set (Var "Q")) "being"   ($#m1_subset_1 :::"PLANE":::) "of" (Set (Var "S")) "holds"   (Bool  "("  (Bool  "("  (Bool (Set (Var "K"))  ($#r3_incsp_1 :::"on"::: )  (Set (Var "Q"))) & (Bool (Set (Var "L"))  ($#r3_incsp_1 :::"on"::: )  (Set (Var "Q")))  ")" ) "iff" (Bool (Set (Var "P"))  ($#r1_hidden :::"="::: )  (Set (Var "Q")))  ")" ))))) ; 
 definitionlet "S" be   ($#l2_incsp_1 :::"IncSpace":::); let "A", "B" be   ($#m1_subset_1 :::"POINT":::) "of" (Set (Const "S")); assume 
(Bool (Set (Const "A"))  ($#r1_hidden :::"<>"::: )  (Set (Const "B")))
 ; func  :::"Line":::  "(" "A" "," "B" ")"  ->   ($#m1_subset_1 :::"LINE":::) "of" "S" means :: INCSP_1:def 19 (Bool (Set  ($#k7_domain_1 :::"{"::: ) "A" "," "B" ($#k7_domain_1 :::"}"::: ) )  ($#r4_incsp_1 :::"on"::: )  it); end; 








:: deftheorem    defines :::"Line"::: INCSP_1:def 19 :  (Bool  "for" (Set (Var "S")) "being"   ($#l2_incsp_1 :::"IncSpace":::)  (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "S"))  "st" (Bool (Bool (Set (Var "A"))  ($#r1_hidden :::"<>"::: )  (Set (Var "B")))) "holds"  (Bool  "for" (Set (Var "b4")) "being"   ($#m1_subset_1 :::"LINE":::) "of" (Set (Var "S")) "holds"   (Bool  "("  (Bool (Set (Var "b4"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_incsp_1 :::"Line"::: )   "(" (Set (Var "A")) "," (Set (Var "B")) ")" )) "iff" (Bool (Set  ($#k7_domain_1 :::"{"::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k7_domain_1 :::"}"::: ) )  ($#r4_incsp_1 :::"on"::: )  (Set (Var "b4")))  ")" )))); 
 definitionlet "S" be   ($#l2_incsp_1 :::"IncSpace":::); let "A", "B", "C" be   ($#m1_subset_1 :::"POINT":::) "of" (Set (Const "S")); assume 
(Bool (Bool  "not" (Set  ($#k8_domain_1 :::"{"::: ) (Set (Const "A")) "," (Set (Const "B")) "," (Set (Const "C")) ($#k8_domain_1 :::"}"::: ) ) "is"   ($#v3_incsp_1 :::"linear"::: )  ))
 ; func  :::"Plane":::  "(" "A" "," "B" "," "C" ")"  ->   ($#m1_subset_1 :::"PLANE":::) "of" "S" means :: INCSP_1:def 20 (Bool (Set  ($#k8_domain_1 :::"{"::: ) "A" "," "B" "," "C" ($#k8_domain_1 :::"}"::: ) )  ($#r5_incsp_1 :::"on"::: )  it); end; 









:: deftheorem    defines :::"Plane"::: INCSP_1:def 20 :  (Bool  "for" (Set (Var "S")) "being"   ($#l2_incsp_1 :::"IncSpace":::)  (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being"   ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "S"))  "st" (Bool (Bool (Bool  "not" (Set  ($#k8_domain_1 :::"{"::: ) (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) ($#k8_domain_1 :::"}"::: ) ) "is"   ($#v3_incsp_1 :::"linear"::: )  ))) "holds"  (Bool  "for" (Set (Var "b5")) "being"   ($#m1_subset_1 :::"PLANE":::) "of" (Set (Var "S")) "holds"   (Bool  "("  (Bool (Set (Var "b5"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_incsp_1 :::"Plane"::: )   "(" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) ")" )) "iff" (Bool (Set  ($#k8_domain_1 :::"{"::: ) (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) ($#k8_domain_1 :::"}"::: ) )  ($#r5_incsp_1 :::"on"::: )  (Set (Var "b5")))  ")" )))); 
 definitionlet "S" be   ($#l2_incsp_1 :::"IncSpace":::); let "A" be   ($#m1_subset_1 :::"POINT":::) "of" (Set (Const "S")); let "L" be   ($#m1_subset_1 :::"LINE":::) "of" (Set (Const "S")); assume 
(Bool (Bool  "not" (Set (Const "A"))  ($#r1_incsp_1 :::"on"::: )  (Set (Const "L"))))
 ; func  :::"Plane":::  "(" "A" "," "L" ")"  ->   ($#m1_subset_1 :::"PLANE":::) "of" "S" means :: INCSP_1:def 21 (Bool  "("  (Bool "A"  ($#r2_incsp_1 :::"on"::: )  it) & (Bool "L"  ($#r3_incsp_1 :::"on"::: )  it)  ")" ); end; 








:: deftheorem    defines :::"Plane"::: INCSP_1:def 21 :  (Bool  "for" (Set (Var "S")) "being"   ($#l2_incsp_1 :::"IncSpace":::)  (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "S"))  (Bool  "for" (Set (Var "L")) "being"   ($#m1_subset_1 :::"LINE":::) "of" (Set (Var "S"))  "st" (Bool (Bool (Bool  "not" (Set (Var "A"))  ($#r1_incsp_1 :::"on"::: )  (Set (Var "L"))))) "holds"  (Bool  "for" (Set (Var "b4")) "being"   ($#m1_subset_1 :::"PLANE":::) "of" (Set (Var "S")) "holds"   (Bool  "("  (Bool (Set (Var "b4"))  ($#r1_hidden :::"="::: )  (Set   ($#k3_incsp_1 :::"Plane"::: )   "(" (Set (Var "A")) "," (Set (Var "L")) ")" )) "iff" (Bool  "("  (Bool (Set (Var "A"))  ($#r2_incsp_1 :::"on"::: )  (Set (Var "b4"))) & (Bool (Set (Var "L"))  ($#r3_incsp_1 :::"on"::: )  (Set (Var "b4")))  ")" )  ")" ))))); 
 definitionlet "S" be   ($#l2_incsp_1 :::"IncSpace":::); let "K", "L" be   ($#m1_subset_1 :::"LINE":::) "of" (Set (Const "S")); assume that  
(Bool (Set (Const "K"))  ($#r1_hidden :::"<>"::: )  (Set (Const "L")))
 and  
(Bool  "ex" (Set (Var "A")) "being"   ($#m1_subset_1 :::"POINT":::) "of" (Set (Const "S")) "st"  (Bool  "("  (Bool (Set (Var "A"))  ($#r1_incsp_1 :::"on"::: )  (Set (Const "K"))) & (Bool (Set (Var "A"))  ($#r1_incsp_1 :::"on"::: )  (Set (Const "L")))  ")" ))
 ; func  :::"Plane":::  "(" "K" "," "L" ")"  ->   ($#m1_subset_1 :::"PLANE":::) "of" "S" means :: INCSP_1:def 22 (Bool  "("  (Bool "K"  ($#r3_incsp_1 :::"on"::: )  it) & (Bool "L"  ($#r3_incsp_1 :::"on"::: )  it)  ")" ); end; 








:: deftheorem    defines :::"Plane"::: INCSP_1:def 22 :  (Bool  "for" (Set (Var "S")) "being"   ($#l2_incsp_1 :::"IncSpace":::)  (Bool  "for" (Set (Var "K")) "," (Set (Var "L")) "being"   ($#m1_subset_1 :::"LINE":::) "of" (Set (Var "S"))  "st" (Bool (Bool (Set (Var "K"))  ($#r1_hidden :::"<>"::: )  (Set (Var "L"))) & (Bool  "ex" (Set (Var "A")) "being"   ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "S")) "st"  (Bool  "("  (Bool (Set (Var "A"))  ($#r1_incsp_1 :::"on"::: )  (Set (Var "K"))) & (Bool (Set (Var "A"))  ($#r1_incsp_1 :::"on"::: )  (Set (Var "L")))  ")" ))) "holds"  (Bool  "for" (Set (Var "b4")) "being"   ($#m1_subset_1 :::"PLANE":::) "of" (Set (Var "S")) "holds"   (Bool  "("  (Bool (Set (Var "b4"))  ($#r1_hidden :::"="::: )  (Set   ($#k4_incsp_1 :::"Plane"::: )   "(" (Set (Var "K")) "," (Set (Var "L")) ")" )) "iff" (Bool  "("  (Bool (Set (Var "K"))  ($#r3_incsp_1 :::"on"::: )  (Set (Var "b4"))) & (Bool (Set (Var "L"))  ($#r3_incsp_1 :::"on"::: )  (Set (Var "b4")))  ")" )  ")" )))); 
 
theorem :: INCSP_1:28 (Bool  "for" (Set (Var "S")) "being"   ($#l2_incsp_1 :::"IncSpace":::)  (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "S"))  "st" (Bool (Bool (Set (Var "A"))  ($#r1_hidden :::"<>"::: )  (Set (Var "B")))) "holds"  (Bool (Set   ($#k1_incsp_1 :::"Line"::: )   "(" (Set (Var "A")) "," (Set (Var "B")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k1_incsp_1 :::"Line"::: )   "(" (Set (Var "B")) "," (Set (Var "A")) ")" )))) ; 
 
theorem :: INCSP_1:29 (Bool  "for" (Set (Var "S")) "being"   ($#l2_incsp_1 :::"IncSpace":::)  (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being"   ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "S"))  "st" (Bool (Bool (Bool  "not" (Set  ($#k8_domain_1 :::"{"::: ) (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) ($#k8_domain_1 :::"}"::: ) ) "is"   ($#v3_incsp_1 :::"linear"::: )  ))) "holds"  (Bool (Set   ($#k2_incsp_1 :::"Plane"::: )   "(" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k2_incsp_1 :::"Plane"::: )   "(" (Set (Var "A")) "," (Set (Var "C")) "," (Set (Var "B")) ")" )))) ; 
 
theorem :: INCSP_1:30 (Bool  "for" (Set (Var "S")) "being"   ($#l2_incsp_1 :::"IncSpace":::)  (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being"   ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "S"))  "st" (Bool (Bool (Bool  "not" (Set  ($#k8_domain_1 :::"{"::: ) (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) ($#k8_domain_1 :::"}"::: ) ) "is"   ($#v3_incsp_1 :::"linear"::: )  ))) "holds"  (Bool (Set   ($#k2_incsp_1 :::"Plane"::: )   "(" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k2_incsp_1 :::"Plane"::: )   "(" (Set (Var "B")) "," (Set (Var "A")) "," (Set (Var "C")) ")" )))) ; 
 
theorem :: INCSP_1:31 (Bool  "for" (Set (Var "S")) "being"   ($#l2_incsp_1 :::"IncSpace":::)  (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being"   ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "S"))  "st" (Bool (Bool (Bool  "not" (Set  ($#k8_domain_1 :::"{"::: ) (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) ($#k8_domain_1 :::"}"::: ) ) "is"   ($#v3_incsp_1 :::"linear"::: )  ))) "holds"  (Bool (Set   ($#k2_incsp_1 :::"Plane"::: )   "(" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k2_incsp_1 :::"Plane"::: )   "(" (Set (Var "B")) "," (Set (Var "C")) "," (Set (Var "A")) ")" )))) ; 
 
theorem :: INCSP_1:32 (Bool  "for" (Set (Var "S")) "being"   ($#l2_incsp_1 :::"IncSpace":::)  (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being"   ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "S"))  "st" (Bool (Bool (Bool  "not" (Set  ($#k8_domain_1 :::"{"::: ) (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) ($#k8_domain_1 :::"}"::: ) ) "is"   ($#v3_incsp_1 :::"linear"::: )  ))) "holds"  (Bool (Set   ($#k2_incsp_1 :::"Plane"::: )   "(" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k2_incsp_1 :::"Plane"::: )   "(" (Set (Var "C")) "," (Set (Var "A")) "," (Set (Var "B")) ")" )))) ; 
 
theorem :: INCSP_1:33 (Bool  "for" (Set (Var "S")) "being"   ($#l2_incsp_1 :::"IncSpace":::)  (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being"   ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "S"))  "st" (Bool (Bool (Bool  "not" (Set  ($#k8_domain_1 :::"{"::: ) (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) ($#k8_domain_1 :::"}"::: ) ) "is"   ($#v3_incsp_1 :::"linear"::: )  ))) "holds"  (Bool (Set   ($#k2_incsp_1 :::"Plane"::: )   "(" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k2_incsp_1 :::"Plane"::: )   "(" (Set (Var "C")) "," (Set (Var "B")) "," (Set (Var "A")) ")" )))) ; 
 
theorem :: INCSP_1:34 (Bool  "for" (Set (Var "S")) "being"   ($#l2_incsp_1 :::"IncSpace":::)  (Bool  "for" (Set (Var "K")) "," (Set (Var "L")) "being"   ($#m1_subset_1 :::"LINE":::) "of" (Set (Var "S"))  "st" (Bool (Bool (Set (Var "K"))  ($#r1_hidden :::"<>"::: )  (Set (Var "L"))) & (Bool  "ex" (Set (Var "A")) "being"   ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "S")) "st"  (Bool  "("  (Bool (Set (Var "A"))  ($#r1_incsp_1 :::"on"::: )  (Set (Var "K"))) & (Bool (Set (Var "A"))  ($#r1_incsp_1 :::"on"::: )  (Set (Var "L")))  ")" ))) "holds"  (Bool (Set   ($#k4_incsp_1 :::"Plane"::: )   "(" (Set (Var "K")) "," (Set (Var "L")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k4_incsp_1 :::"Plane"::: )   "(" (Set (Var "L")) "," (Set (Var "K")) ")" )))) ; 
 
theorem :: INCSP_1:35 (Bool  "for" (Set (Var "S")) "being"   ($#l2_incsp_1 :::"IncSpace":::)  (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being"   ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "S"))  "st" (Bool (Bool (Set (Var "A"))  ($#r1_hidden :::"<>"::: )  (Set (Var "B"))) & (Bool (Set (Var "C"))  ($#r1_incsp_1 :::"on"::: )  (Set   ($#k1_incsp_1 :::"Line"::: )   "(" (Set (Var "A")) "," (Set (Var "B")) ")" ))) "holds"  (Bool (Set  ($#k8_domain_1 :::"{"::: ) (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) ($#k8_domain_1 :::"}"::: ) ) "is"   ($#v3_incsp_1 :::"linear"::: )  ))) ; 
 
theorem :: INCSP_1:36 (Bool  "for" (Set (Var "S")) "being"   ($#l2_incsp_1 :::"IncSpace":::)  (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being"   ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "S"))  "st" (Bool (Bool (Set (Var "A"))  ($#r1_hidden :::"<>"::: )  (Set (Var "B"))) & (Bool (Set (Var "A"))  ($#r1_hidden :::"<>"::: )  (Set (Var "C"))) & (Bool (Set  ($#k8_domain_1 :::"{"::: ) (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) ($#k8_domain_1 :::"}"::: ) ) "is"   ($#v3_incsp_1 :::"linear"::: )  )) "holds"  (Bool (Set   ($#k1_incsp_1 :::"Line"::: )   "(" (Set (Var "A")) "," (Set (Var "B")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k1_incsp_1 :::"Line"::: )   "(" (Set (Var "A")) "," (Set (Var "C")) ")" )))) ; 
 
theorem :: INCSP_1:37 (Bool  "for" (Set (Var "S")) "being"   ($#l2_incsp_1 :::"IncSpace":::)  (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being"   ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "S"))  "st" (Bool (Bool (Bool  "not" (Set  ($#k8_domain_1 :::"{"::: ) (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) ($#k8_domain_1 :::"}"::: ) ) "is"   ($#v3_incsp_1 :::"linear"::: )  ))) "holds"  (Bool (Set   ($#k2_incsp_1 :::"Plane"::: )   "(" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k3_incsp_1 :::"Plane"::: )   "(" (Set (Var "C")) "," (Set  "("  ($#k1_incsp_1 :::"Line"::: )   "(" (Set (Var "A")) "," (Set (Var "B")) ")"  ")" ) ")" )))) ; 
 
theorem :: INCSP_1:38 (Bool  "for" (Set (Var "S")) "being"   ($#l2_incsp_1 :::"IncSpace":::)  (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "," (Set (Var "D")) "being"   ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "S"))  "st" (Bool (Bool (Bool  "not" (Set  ($#k8_domain_1 :::"{"::: ) (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) ($#k8_domain_1 :::"}"::: ) ) "is"   ($#v3_incsp_1 :::"linear"::: )  )) & (Bool (Set (Var "D"))  ($#r2_incsp_1 :::"on"::: )  (Set   ($#k2_incsp_1 :::"Plane"::: )   "(" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) ")" ))) "holds"  (Bool (Set  ($#k9_domain_1 :::"{"::: ) (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "," (Set (Var "D")) ($#k9_domain_1 :::"}"::: ) ) "is"   ($#v4_incsp_1 :::"planar"::: )  ))) ; 
 
theorem :: INCSP_1:39 (Bool  "for" (Set (Var "S")) "being"   ($#l2_incsp_1 :::"IncSpace":::)  (Bool  "for" (Set (Var "C")) "," (Set (Var "A")) "," (Set (Var "B")) "being"   ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "S"))  (Bool  "for" (Set (Var "L")) "being"   ($#m1_subset_1 :::"LINE":::) "of" (Set (Var "S"))  "st" (Bool (Bool (Bool  "not" (Set (Var "C"))  ($#r1_incsp_1 :::"on"::: )  (Set (Var "L")))) & (Bool (Set  ($#k7_domain_1 :::"{"::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k7_domain_1 :::"}"::: ) )  ($#r4_incsp_1 :::"on"::: )  (Set (Var "L"))) & (Bool (Set (Var "A"))  ($#r1_hidden :::"<>"::: )  (Set (Var "B")))) "holds"  (Bool (Set   ($#k3_incsp_1 :::"Plane"::: )   "(" (Set (Var "C")) "," (Set (Var "L")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k2_incsp_1 :::"Plane"::: )   "(" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) ")" ))))) ; 
 
theorem :: INCSP_1:40 (Bool  "for" (Set (Var "S")) "being"   ($#l2_incsp_1 :::"IncSpace":::)  (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being"   ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "S"))  "st" (Bool (Bool (Bool  "not" (Set  ($#k8_domain_1 :::"{"::: ) (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) ($#k8_domain_1 :::"}"::: ) ) "is"   ($#v3_incsp_1 :::"linear"::: )  ))) "holds"  (Bool (Set   ($#k2_incsp_1 :::"Plane"::: )   "(" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k4_incsp_1 :::"Plane"::: )   "(" (Set  "("  ($#k1_incsp_1 :::"Line"::: )   "(" (Set (Var "A")) "," (Set (Var "B")) ")"  ")" ) "," (Set  "("  ($#k1_incsp_1 :::"Line"::: )   "(" (Set (Var "A")) "," (Set (Var "C")) ")"  ")" ) ")" )))) ; 
 
theorem :: INCSP_1:41 (Bool  "for" (Set (Var "S")) "being"   ($#l2_incsp_1 :::"IncSpace":::)  (Bool  "for" (Set (Var "P")) "being"   ($#m1_subset_1 :::"PLANE":::) "of" (Set (Var "S")) (Bool  "ex" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being"   ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "S")) "st"  (Bool  "("  (Bool (Set  ($#k8_domain_1 :::"{"::: ) (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) ($#k8_domain_1 :::"}"::: ) )  ($#r5_incsp_1 :::"on"::: )  (Set (Var "P"))) & (Bool (Bool  "not" (Set  ($#k8_domain_1 :::"{"::: ) (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) ($#k8_domain_1 :::"}"::: ) ) "is"   ($#v3_incsp_1 :::"linear"::: )  ))  ")" )))) ; 
 
theorem :: INCSP_1:42 (Bool  "for" (Set (Var "S")) "being"   ($#l2_incsp_1 :::"IncSpace":::)  (Bool  "for" (Set (Var "P")) "being"   ($#m1_subset_1 :::"PLANE":::) "of" (Set (Var "S")) (Bool  "ex" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "," (Set (Var "D")) "being"   ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "S")) "st"  (Bool  "("  (Bool (Set (Var "A"))  ($#r2_incsp_1 :::"on"::: )  (Set (Var "P"))) & (Bool (Bool  "not" (Set  ($#k9_domain_1 :::"{"::: ) (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "," (Set (Var "D")) ($#k9_domain_1 :::"}"::: ) ) "is"   ($#v4_incsp_1 :::"planar"::: )  ))  ")" )))) ; 
 
theorem :: INCSP_1:43 (Bool  "for" (Set (Var "S")) "being"   ($#l2_incsp_1 :::"IncSpace":::)  (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "S"))  (Bool  "for" (Set (Var "L")) "being"   ($#m1_subset_1 :::"LINE":::) "of" (Set (Var "S")) (Bool  "ex" (Set (Var "B")) "being"   ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "S")) "st"  (Bool  "("  (Bool (Set (Var "A"))  ($#r1_hidden :::"<>"::: )  (Set (Var "B"))) & (Bool (Set (Var "B"))  ($#r1_incsp_1 :::"on"::: )  (Set (Var "L")))  ")" ))))) ; 
 
theorem :: INCSP_1:44 (Bool  "for" (Set (Var "S")) "being"   ($#l2_incsp_1 :::"IncSpace":::)  (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "S"))  (Bool  "for" (Set (Var "P")) "being"   ($#m1_subset_1 :::"PLANE":::) "of" (Set (Var "S"))  "st" (Bool (Bool (Set (Var "A"))  ($#r1_hidden :::"<>"::: )  (Set (Var "B")))) "holds"  (Bool  "ex" (Set (Var "C")) "being"   ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "S")) "st"  (Bool  "("  (Bool (Set (Var "C"))  ($#r2_incsp_1 :::"on"::: )  (Set (Var "P"))) & (Bool (Bool  "not" (Set  ($#k8_domain_1 :::"{"::: ) (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) ($#k8_domain_1 :::"}"::: ) ) "is"   ($#v3_incsp_1 :::"linear"::: )  ))  ")" ))))) ; 
 
theorem :: INCSP_1:45 (Bool  "for" (Set (Var "S")) "being"   ($#l2_incsp_1 :::"IncSpace":::)  (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being"   ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "S"))  "st" (Bool (Bool (Bool  "not" (Set  ($#k8_domain_1 :::"{"::: ) (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) ($#k8_domain_1 :::"}"::: ) ) "is"   ($#v3_incsp_1 :::"linear"::: )  ))) "holds"  (Bool  "ex" (Set (Var "D")) "being"   ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "S")) "st" (Bool (Bool  "not" (Set  ($#k9_domain_1 :::"{"::: ) (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "," (Set (Var "D")) ($#k9_domain_1 :::"}"::: ) ) "is"   ($#v4_incsp_1 :::"planar"::: )  ))))) ; 
 
theorem :: INCSP_1:46 (Bool  "for" (Set (Var "S")) "being"   ($#l2_incsp_1 :::"IncSpace":::)  (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "S"))  (Bool  "for" (Set (Var "P")) "being"   ($#m1_subset_1 :::"PLANE":::) "of" (Set (Var "S")) (Bool  "ex" (Set (Var "B")) "," (Set (Var "C")) "being"   ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "S")) "st"  (Bool  "("  (Bool (Set  ($#k7_domain_1 :::"{"::: ) (Set (Var "B")) "," (Set (Var "C")) ($#k7_domain_1 :::"}"::: ) )  ($#r5_incsp_1 :::"on"::: )  (Set (Var "P"))) & (Bool (Bool  "not" (Set  ($#k8_domain_1 :::"{"::: ) (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) ($#k8_domain_1 :::"}"::: ) ) "is"   ($#v3_incsp_1 :::"linear"::: )  ))  ")" ))))) ; 
 
theorem :: INCSP_1:47 (Bool  "for" (Set (Var "S")) "being"   ($#l2_incsp_1 :::"IncSpace":::)  (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "S"))  "st" (Bool (Bool (Set (Var "A"))  ($#r1_hidden :::"<>"::: )  (Set (Var "B")))) "holds"  (Bool  "ex" (Set (Var "C")) "," (Set (Var "D")) "being"   ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "S")) "st" (Bool (Bool  "not" (Set  ($#k9_domain_1 :::"{"::: ) (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "," (Set (Var "D")) ($#k9_domain_1 :::"}"::: ) ) "is"   ($#v4_incsp_1 :::"planar"::: )  ))))) ; 
 
theorem :: INCSP_1:48 (Bool  "for" (Set (Var "S")) "being"   ($#l2_incsp_1 :::"IncSpace":::)  (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "S"))  "holds"  (Bool  "not" (Bool  "for" (Set (Var "B")) "," (Set (Var "C")) "," (Set (Var "D")) "being"   ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "S")) "holds"  (Bool (Set  ($#k9_domain_1 :::"{"::: ) (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "," (Set (Var "D")) ($#k9_domain_1 :::"}"::: ) ) "is"   ($#v4_incsp_1 :::"planar"::: )  ))))) ; 
 
theorem :: INCSP_1:49 (Bool  "for" (Set (Var "S")) "being"   ($#l2_incsp_1 :::"IncSpace":::)  (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "S"))  (Bool  "for" (Set (Var "P")) "being"   ($#m1_subset_1 :::"PLANE":::) "of" (Set (Var "S")) (Bool  "ex" (Set (Var "L")) "being"   ($#m1_subset_1 :::"LINE":::) "of" (Set (Var "S")) "st"  (Bool  "("  (Bool (Bool  "not" (Set (Var "A"))  ($#r1_incsp_1 :::"on"::: )  (Set (Var "L")))) & (Bool (Set (Var "L"))  ($#r3_incsp_1 :::"on"::: )  (Set (Var "P")))  ")" ))))) ; 
 
theorem :: INCSP_1:50 (Bool  "for" (Set (Var "S")) "being"   ($#l2_incsp_1 :::"IncSpace":::)  (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "S"))  (Bool  "for" (Set (Var "P")) "being"   ($#m1_subset_1 :::"PLANE":::) "of" (Set (Var "S"))  "st" (Bool (Bool (Set (Var "A"))  ($#r2_incsp_1 :::"on"::: )  (Set (Var "P")))) "holds"  (Bool  "ex" (Set (Var "L")) "," (Set (Var "L1")) "," (Set (Var "L2")) "being"   ($#m1_subset_1 :::"LINE":::) "of" (Set (Var "S")) "st"  (Bool  "("  (Bool (Set (Var "L1"))  ($#r1_hidden :::"<>"::: )  (Set (Var "L2"))) & (Bool (Set (Var "L1"))  ($#r3_incsp_1 :::"on"::: )  (Set (Var "P"))) & (Bool (Set (Var "L2"))  ($#r3_incsp_1 :::"on"::: )  (Set (Var "P"))) & (Bool (Bool  "not" (Set (Var "L"))  ($#r3_incsp_1 :::"on"::: )  (Set (Var "P")))) & (Bool (Set (Var "A"))  ($#r1_incsp_1 :::"on"::: )  (Set (Var "L"))) & (Bool (Set (Var "A"))  ($#r1_incsp_1 :::"on"::: )  (Set (Var "L1"))) & (Bool (Set (Var "A"))  ($#r1_incsp_1 :::"on"::: )  (Set (Var "L2")))  ")" ))))) ; 
 
theorem :: INCSP_1:51 (Bool  "for" (Set (Var "S")) "being"   ($#l2_incsp_1 :::"IncSpace":::)  (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "S")) (Bool  "ex" (Set (Var "L")) "," (Set (Var "L1")) "," (Set (Var "L2")) "being"   ($#m1_subset_1 :::"LINE":::) "of" (Set (Var "S")) "st"  (Bool  "("  (Bool (Set (Var "A"))  ($#r1_incsp_1 :::"on"::: )  (Set (Var "L"))) & (Bool (Set (Var "A"))  ($#r1_incsp_1 :::"on"::: )  (Set (Var "L1"))) & (Bool (Set (Var "A"))  ($#r1_incsp_1 :::"on"::: )  (Set (Var "L2"))) & (Bool  "("   "for" (Set (Var "P")) "being"   ($#m1_subset_1 :::"PLANE":::) "of" (Set (Var "S"))  "holds"  (Bool  "("   "not" (Bool (Set (Var "L"))  ($#r3_incsp_1 :::"on"::: )  (Set (Var "P"))) "or"  "not" (Bool (Set (Var "L1"))  ($#r3_incsp_1 :::"on"::: )  (Set (Var "P"))) "or"  "not" (Bool (Set (Var "L2"))  ($#r3_incsp_1 :::"on"::: )  (Set (Var "P")))  ")" )  ")" )  ")" )))) ; 
 
theorem :: INCSP_1:52 (Bool  "for" (Set (Var "S")) "being"   ($#l2_incsp_1 :::"IncSpace":::)  (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "S"))  (Bool  "for" (Set (Var "L")) "being"   ($#m1_subset_1 :::"LINE":::) "of" (Set (Var "S")) (Bool  "ex" (Set (Var "P")) "being"   ($#m1_subset_1 :::"PLANE":::) "of" (Set (Var "S")) "st"  (Bool  "("  (Bool (Set (Var "A"))  ($#r2_incsp_1 :::"on"::: )  (Set (Var "P"))) & (Bool (Bool  "not" (Set (Var "L"))  ($#r3_incsp_1 :::"on"::: )  (Set (Var "P"))))  ")" ))))) ; 
 
theorem :: INCSP_1:53 (Bool  "for" (Set (Var "S")) "being"   ($#l2_incsp_1 :::"IncSpace":::)  (Bool  "for" (Set (Var "L")) "being"   ($#m1_subset_1 :::"LINE":::) "of" (Set (Var "S"))  (Bool  "for" (Set (Var "P")) "being"   ($#m1_subset_1 :::"PLANE":::) "of" (Set (Var "S")) (Bool  "ex" (Set (Var "A")) "being"   ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "S")) "st"  (Bool  "("  (Bool (Set (Var "A"))  ($#r2_incsp_1 :::"on"::: )  (Set (Var "P"))) & (Bool (Bool  "not" (Set (Var "A"))  ($#r1_incsp_1 :::"on"::: )  (Set (Var "L"))))  ")" ))))) ; 
 
theorem :: INCSP_1:54 (Bool  "for" (Set (Var "S")) "being"   ($#l2_incsp_1 :::"IncSpace":::)  (Bool  "for" (Set (Var "L")) "being"   ($#m1_subset_1 :::"LINE":::) "of" (Set (Var "S")) (Bool  "ex" (Set (Var "K")) "being"   ($#m1_subset_1 :::"LINE":::) "of" (Set (Var "S")) "st"  (Bool  "for" (Set (Var "P")) "being"   ($#m1_subset_1 :::"PLANE":::) "of" (Set (Var "S"))  "holds"  (Bool  "("   "not" (Bool (Set (Var "L"))  ($#r3_incsp_1 :::"on"::: )  (Set (Var "P"))) "or"  "not" (Bool (Set (Var "K"))  ($#r3_incsp_1 :::"on"::: )  (Set (Var "P")))  ")" ))))) ; 
 
theorem :: INCSP_1:55 (Bool  "for" (Set (Var "S")) "being"   ($#l2_incsp_1 :::"IncSpace":::)  (Bool  "for" (Set (Var "L")) "being"   ($#m1_subset_1 :::"LINE":::) "of" (Set (Var "S")) (Bool  "ex" (Set (Var "P")) "," (Set (Var "Q")) "being"   ($#m1_subset_1 :::"PLANE":::) "of" (Set (Var "S")) "st"  (Bool  "("  (Bool (Set (Var "P"))  ($#r1_hidden :::"<>"::: )  (Set (Var "Q"))) & (Bool (Set (Var "L"))  ($#r3_incsp_1 :::"on"::: )  (Set (Var "P"))) & (Bool (Set (Var "L"))  ($#r3_incsp_1 :::"on"::: )  (Set (Var "Q")))  ")" )))) ; 
 
theorem :: INCSP_1:56 (Bool  "for" (Set (Var "S")) "being"   ($#l2_incsp_1 :::"IncSpace":::)  (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "S"))  (Bool  "for" (Set (Var "L")) "being"   ($#m1_subset_1 :::"LINE":::) "of" (Set (Var "S"))  (Bool  "for" (Set (Var "P")) "being"   ($#m1_subset_1 :::"PLANE":::) "of" (Set (Var "S"))  "st" (Bool (Bool (Bool  "not" (Set (Var "L"))  ($#r3_incsp_1 :::"on"::: )  (Set (Var "P")))) & (Bool (Set  ($#k7_domain_1 :::"{"::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k7_domain_1 :::"}"::: ) )  ($#r4_incsp_1 :::"on"::: )  (Set (Var "L"))) & (Bool (Set  ($#k7_domain_1 :::"{"::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k7_domain_1 :::"}"::: ) )  ($#r5_incsp_1 :::"on"::: )  (Set (Var "P")))) "holds"  (Bool (Set (Var "A"))  ($#r1_hidden :::"="::: )  (Set (Var "B"))))))) ; 
 
theorem :: INCSP_1:57 (Bool  "for" (Set (Var "S")) "being"   ($#l2_incsp_1 :::"IncSpace":::)  (Bool  "for" (Set (Var "P")) "," (Set (Var "Q")) "being"   ($#m1_subset_1 :::"PLANE":::) "of" (Set (Var "S"))  "holds"  (Bool  "("   "not" (Bool (Set (Var "P"))  ($#r1_hidden :::"<>"::: )  (Set (Var "Q"))) "or" (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "S"))  "holds"  (Bool  "("   "not" (Bool (Set (Var "A"))  ($#r2_incsp_1 :::"on"::: )  (Set (Var "P"))) "or"  "not" (Bool (Set (Var "A"))  ($#r2_incsp_1 :::"on"::: )  (Set (Var "Q")))  ")" )) "or" (Bool  "ex" (Set (Var "L")) "being"   ($#m1_subset_1 :::"LINE":::) "of" (Set (Var "S")) "st"  (Bool  "for" (Set (Var "B")) "being"   ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "S")) "holds"   (Bool  "("  (Bool  "("  (Bool (Set (Var "B"))  ($#r2_incsp_1 :::"on"::: )  (Set (Var "P"))) & (Bool (Set (Var "B"))  ($#r2_incsp_1 :::"on"::: )  (Set (Var "Q")))  ")" ) "iff" (Bool (Set (Var "B"))  ($#r1_incsp_1 :::"on"::: )  (Set (Var "L")))  ")" )))  ")" ))) ;