:: PROJDES1  semantic presentation begin  























theorem :: PROJDES1:1 (Bool  "for" (Set (Var "FCPS")) "being"   ($#v7_anproj_2 :::"up-3-dimensional"::: )    ($#l1_collsp :::"CollProjectiveSpace":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "FCPS"))  "st" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c"))  ($#r1_collsp :::"is_collinear"::: )  )) "holds"  (Bool  "("  (Bool (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "a"))  ($#r1_collsp :::"is_collinear"::: )  ) & (Bool (Set (Var "c")) "," (Set (Var "a")) "," (Set (Var "b"))  ($#r1_collsp :::"is_collinear"::: )  ) & (Bool (Set (Var "b")) "," (Set (Var "a")) "," (Set (Var "c"))  ($#r1_collsp :::"is_collinear"::: )  ) & (Bool (Set (Var "a")) "," (Set (Var "c")) "," (Set (Var "b"))  ($#r1_collsp :::"is_collinear"::: )  ) & (Bool (Set (Var "c")) "," (Set (Var "b")) "," (Set (Var "a"))  ($#r1_collsp :::"is_collinear"::: )  )  ")" ))) ; 
 
theorem :: PROJDES1:2 (Bool  "for" (Set (Var "FCPS")) "being"   ($#v7_anproj_2 :::"up-3-dimensional"::: )    ($#l1_collsp :::"CollProjectiveSpace":::)  (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "FCPS"))  "holds"  (Bool  "not" (Bool  "for" (Set (Var "q")) "," (Set (Var "r")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "FCPS")) "holds"  (Bool (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r"))  ($#r1_collsp :::"is_collinear"::: )  ))))) ; 
 
theorem :: PROJDES1:3 (Bool  "for" (Set (Var "FCPS")) "being"   ($#v7_anproj_2 :::"up-3-dimensional"::: )    ($#l1_collsp :::"CollProjectiveSpace":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "b9")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "FCPS"))  "st" (Bool (Bool (Bool  "not" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c"))  ($#r1_collsp :::"is_collinear"::: )  )) & (Bool (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "b9"))  ($#r1_collsp :::"is_collinear"::: )  ) & (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set (Var "b9")))) "holds"  (Bool  "not" (Bool (Set (Var "a")) "," (Set (Var "b9")) "," (Set (Var "c"))  ($#r1_collsp :::"is_collinear"::: )  )))) ; 
 
theorem :: PROJDES1:4 (Bool  "for" (Set (Var "FCPS")) "being"   ($#v7_anproj_2 :::"up-3-dimensional"::: )    ($#l1_collsp :::"CollProjectiveSpace":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "FCPS"))  "st" (Bool (Bool (Bool  "not" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c"))  ($#r1_collsp :::"is_collinear"::: )  )) & (Bool (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "d"))  ($#r1_collsp :::"is_collinear"::: )  ) & (Bool (Set (Var "a")) "," (Set (Var "c")) "," (Set (Var "d"))  ($#r1_collsp :::"is_collinear"::: )  )) "holds"  (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set (Var "d"))))) ; 
 
theorem :: PROJDES1:5 (Bool  "for" (Set (Var "FCPS")) "being"   ($#v7_anproj_2 :::"up-3-dimensional"::: )    ($#l1_collsp :::"CollProjectiveSpace":::)  (Bool  "for" (Set (Var "o")) "," (Set (Var "a")) "," (Set (Var "d")) "," (Set (Var "d9")) "," (Set (Var "a9")) "," (Set (Var "s")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "FCPS"))  "st" (Bool (Bool (Bool  "not" (Set (Var "o")) "," (Set (Var "a")) "," (Set (Var "d"))  ($#r1_collsp :::"is_collinear"::: )  )) & (Bool (Set (Var "o")) "," (Set (Var "d")) "," (Set (Var "d9"))  ($#r1_collsp :::"is_collinear"::: )  ) & (Bool (Set (Var "d"))  ($#r1_hidden :::"<>"::: )  (Set (Var "d9"))) & (Bool (Set (Var "a9")) "," (Set (Var "d9")) "," (Set (Var "s"))  ($#r1_collsp :::"is_collinear"::: )  ) & (Bool (Set (Var "o")) "," (Set (Var "a")) "," (Set (Var "a9"))  ($#r1_collsp :::"is_collinear"::: )  ) & (Bool (Set (Var "o"))  ($#r1_hidden :::"<>"::: )  (Set (Var "a9")))) "holds"  (Bool (Set (Var "s"))  ($#r1_hidden :::"<>"::: )  (Set (Var "d"))))) ; 
 definitionlet "FCPS" be   ($#v7_anproj_2 :::"up-3-dimensional"::: )    ($#l1_collsp :::"CollProjectiveSpace":::); let "a", "b", "c", "d" be   ($#m1_subset_1 :::"Element":::) "of" (Set (Const "FCPS")); pred "a" "," "b" "," "c" "," "d" :::"are_coplanar":::  means :: PROJDES1:def 1 (Bool  "ex" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" "FCPS" "st"  (Bool  "("  (Bool "a" "," "b" "," (Set (Var "x"))  ($#r1_collsp :::"is_collinear"::: )  ) & (Bool "c" "," "d" "," (Set (Var "x"))  ($#r1_collsp :::"is_collinear"::: )  )  ")" )); end; 








:: deftheorem    defines :::"are_coplanar"::: PROJDES1:def 1 :  (Bool  "for" (Set (Var "FCPS")) "being"   ($#v7_anproj_2 :::"up-3-dimensional"::: )    ($#l1_collsp :::"CollProjectiveSpace":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "FCPS")) "holds"   (Bool  "("  (Bool (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d"))  ($#r1_projdes1 :::"are_coplanar"::: )  ) "iff" (Bool  "ex" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "FCPS")) "st"  (Bool  "("  (Bool (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "x"))  ($#r1_collsp :::"is_collinear"::: )  ) & (Bool (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "x"))  ($#r1_collsp :::"is_collinear"::: )  )  ")" ))  ")" ))); 
 
theorem :: PROJDES1:6 (Bool  "for" (Set (Var "FCPS")) "being"   ($#v7_anproj_2 :::"up-3-dimensional"::: )    ($#l1_collsp :::"CollProjectiveSpace":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "FCPS"))  "st" (Bool (Bool  "("  (Bool (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c"))  ($#r1_collsp :::"is_collinear"::: )  ) "or" (Bool (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d"))  ($#r1_collsp :::"is_collinear"::: )  ) "or" (Bool (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "a"))  ($#r1_collsp :::"is_collinear"::: )  ) "or" (Bool (Set (Var "d")) "," (Set (Var "a")) "," (Set (Var "b"))  ($#r1_collsp :::"is_collinear"::: )  )  ")" )) "holds"  (Bool (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d"))  ($#r1_projdes1 :::"are_coplanar"::: )  ))) ; 
 
theorem :: PROJDES1:7 (Bool  "for" (Set (Var "FCPS")) "being"   ($#v7_anproj_2 :::"up-3-dimensional"::: )    ($#l1_collsp :::"CollProjectiveSpace":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "FCPS"))  "st" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d"))  ($#r1_projdes1 :::"are_coplanar"::: )  )) "holds"  (Bool  "("  (Bool (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "a"))  ($#r1_projdes1 :::"are_coplanar"::: )  ) & (Bool (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "a")) "," (Set (Var "b"))  ($#r1_projdes1 :::"are_coplanar"::: )  ) & (Bool (Set (Var "d")) "," (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c"))  ($#r1_projdes1 :::"are_coplanar"::: )  ) & (Bool (Set (Var "b")) "," (Set (Var "a")) "," (Set (Var "c")) "," (Set (Var "d"))  ($#r1_projdes1 :::"are_coplanar"::: )  ) & (Bool (Set (Var "c")) "," (Set (Var "b")) "," (Set (Var "d")) "," (Set (Var "a"))  ($#r1_projdes1 :::"are_coplanar"::: )  ) & (Bool (Set (Var "d")) "," (Set (Var "c")) "," (Set (Var "a")) "," (Set (Var "b"))  ($#r1_projdes1 :::"are_coplanar"::: )  ) & (Bool (Set (Var "a")) "," (Set (Var "d")) "," (Set (Var "b")) "," (Set (Var "c"))  ($#r1_projdes1 :::"are_coplanar"::: )  ) & (Bool (Set (Var "a")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "b"))  ($#r1_projdes1 :::"are_coplanar"::: )  ) & (Bool (Set (Var "b")) "," (Set (Var "d")) "," (Set (Var "a")) "," (Set (Var "c"))  ($#r1_projdes1 :::"are_coplanar"::: )  ) & (Bool (Set (Var "c")) "," (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "d"))  ($#r1_projdes1 :::"are_coplanar"::: )  ) & (Bool (Set (Var "d")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "a"))  ($#r1_projdes1 :::"are_coplanar"::: )  ) & (Bool (Set (Var "c")) "," (Set (Var "a")) "," (Set (Var "d")) "," (Set (Var "b"))  ($#r1_projdes1 :::"are_coplanar"::: )  ) & (Bool (Set (Var "d")) "," (Set (Var "b")) "," (Set (Var "a")) "," (Set (Var "c"))  ($#r1_projdes1 :::"are_coplanar"::: )  ) & (Bool (Set (Var "a")) "," (Set (Var "c")) "," (Set (Var "b")) "," (Set (Var "d"))  ($#r1_projdes1 :::"are_coplanar"::: )  ) & (Bool (Set (Var "b")) "," (Set (Var "d")) "," (Set (Var "c")) "," (Set (Var "a"))  ($#r1_projdes1 :::"are_coplanar"::: )  ) & (Bool (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "d")) "," (Set (Var "c"))  ($#r1_projdes1 :::"are_coplanar"::: )  ) & (Bool (Set (Var "a")) "," (Set (Var "d")) "," (Set (Var "c")) "," (Set (Var "b"))  ($#r1_projdes1 :::"are_coplanar"::: )  ) & (Bool (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "a")) "," (Set (Var "d"))  ($#r1_projdes1 :::"are_coplanar"::: )  ) & (Bool (Set (Var "b")) "," (Set (Var "a")) "," (Set (Var "d")) "," (Set (Var "c"))  ($#r1_projdes1 :::"are_coplanar"::: )  ) & (Bool (Set (Var "c")) "," (Set (Var "b")) "," (Set (Var "a")) "," (Set (Var "d"))  ($#r1_projdes1 :::"are_coplanar"::: )  ) & (Bool (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "b")) "," (Set (Var "a"))  ($#r1_projdes1 :::"are_coplanar"::: )  ) & (Bool (Set (Var "d")) "," (Set (Var "a")) "," (Set (Var "c")) "," (Set (Var "b"))  ($#r1_projdes1 :::"are_coplanar"::: )  ) & (Bool (Set (Var "d")) "," (Set (Var "c")) "," (Set (Var "b")) "," (Set (Var "a"))  ($#r1_projdes1 :::"are_coplanar"::: )  )  ")" ))) ; 
 
theorem :: PROJDES1:8 (Bool  "for" (Set (Var "FCPS")) "being"   ($#v7_anproj_2 :::"up-3-dimensional"::: )    ($#l1_collsp :::"CollProjectiveSpace":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "," (Set (Var "s")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "FCPS"))  "st" (Bool (Bool (Bool  "not" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c"))  ($#r1_collsp :::"is_collinear"::: )  )) & (Bool (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "p"))  ($#r1_projdes1 :::"are_coplanar"::: )  ) & (Bool (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "q"))  ($#r1_projdes1 :::"are_coplanar"::: )  ) & (Bool (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "r"))  ($#r1_projdes1 :::"are_coplanar"::: )  ) & (Bool (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "s"))  ($#r1_projdes1 :::"are_coplanar"::: )  )) "holds"  (Bool (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "," (Set (Var "s"))  ($#r1_projdes1 :::"are_coplanar"::: )  ))) ; 
 
theorem :: PROJDES1:9 (Bool  "for" (Set (Var "FCPS")) "being"   ($#v7_anproj_2 :::"up-3-dimensional"::: )    ($#l1_collsp :::"CollProjectiveSpace":::)  (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "," (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "s")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "FCPS"))  "st" (Bool (Bool (Bool  "not" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r"))  ($#r1_collsp :::"is_collinear"::: )  )) & (Bool (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "p"))  ($#r1_projdes1 :::"are_coplanar"::: )  ) & (Bool (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "r"))  ($#r1_projdes1 :::"are_coplanar"::: )  ) & (Bool (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "q"))  ($#r1_projdes1 :::"are_coplanar"::: )  ) & (Bool (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "," (Set (Var "s"))  ($#r1_projdes1 :::"are_coplanar"::: )  )) "holds"  (Bool (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "s"))  ($#r1_projdes1 :::"are_coplanar"::: )  ))) ; 
 
theorem :: PROJDES1:10 (Bool  "for" (Set (Var "FCPS")) "being"   ($#v7_anproj_2 :::"up-3-dimensional"::: )    ($#l1_collsp :::"CollProjectiveSpace":::)  (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "," (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "FCPS"))  "st" (Bool (Bool (Set (Var "p"))  ($#r1_hidden :::"<>"::: )  (Set (Var "q"))) & (Bool (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r"))  ($#r1_collsp :::"is_collinear"::: )  ) & (Bool (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "p"))  ($#r1_projdes1 :::"are_coplanar"::: )  ) & (Bool (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "q"))  ($#r1_projdes1 :::"are_coplanar"::: )  )) "holds"  (Bool (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "r"))  ($#r1_projdes1 :::"are_coplanar"::: )  ))) ; 
 
theorem :: PROJDES1:11 (Bool  "for" (Set (Var "FCPS")) "being"   ($#v7_anproj_2 :::"up-3-dimensional"::: )    ($#l1_collsp :::"CollProjectiveSpace":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "," (Set (Var "s")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "FCPS"))  "st" (Bool (Bool (Bool  "not" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c"))  ($#r1_collsp :::"is_collinear"::: )  )) & (Bool (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "p"))  ($#r1_projdes1 :::"are_coplanar"::: )  ) & (Bool (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "q"))  ($#r1_projdes1 :::"are_coplanar"::: )  ) & (Bool (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "r"))  ($#r1_projdes1 :::"are_coplanar"::: )  ) & (Bool (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "s"))  ($#r1_projdes1 :::"are_coplanar"::: )  )) "holds"  (Bool  "ex" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "FCPS")) "st"  (Bool  "("  (Bool (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "x"))  ($#r1_collsp :::"is_collinear"::: )  ) & (Bool (Set (Var "r")) "," (Set (Var "s")) "," (Set (Var "x"))  ($#r1_collsp :::"is_collinear"::: )  )  ")" )))) ; 
 
theorem :: PROJDES1:12 (Bool  "for" (Set (Var "FCPS")) "being"   ($#v7_anproj_2 :::"up-3-dimensional"::: )    ($#l1_collsp :::"CollProjectiveSpace":::)  "holds"  (Bool  "not" (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "FCPS")) "holds"  (Bool (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d"))  ($#r1_projdes1 :::"are_coplanar"::: )  )))) ; 
 
theorem :: PROJDES1:13 (Bool  "for" (Set (Var "FCPS")) "being"   ($#v7_anproj_2 :::"up-3-dimensional"::: )    ($#l1_collsp :::"CollProjectiveSpace":::)  (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "FCPS"))  "st" (Bool (Bool (Bool  "not" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r"))  ($#r1_collsp :::"is_collinear"::: )  ))) "holds"  (Bool  "ex" (Set (Var "s")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "FCPS")) "st" (Bool (Bool  "not" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "," (Set (Var "s"))  ($#r1_projdes1 :::"are_coplanar"::: )  ))))) ; 
 
theorem :: PROJDES1:14 (Bool  "for" (Set (Var "FCPS")) "being"   ($#v7_anproj_2 :::"up-3-dimensional"::: )    ($#l1_collsp :::"CollProjectiveSpace":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "FCPS"))  "st" (Bool (Bool  "("  (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set (Var "b"))) "or" (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set (Var "c"))) "or" (Bool (Set (Var "b"))  ($#r1_hidden :::"="::: )  (Set (Var "c"))) "or" (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set (Var "d"))) "or" (Bool (Set (Var "b"))  ($#r1_hidden :::"="::: )  (Set (Var "d"))) "or" (Bool (Set (Var "d"))  ($#r1_hidden :::"="::: )  (Set (Var "c")))  ")" )) "holds"  (Bool (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d"))  ($#r1_projdes1 :::"are_coplanar"::: )  ))) ; 
 
theorem :: PROJDES1:15 (Bool  "for" (Set (Var "FCPS")) "being"   ($#v7_anproj_2 :::"up-3-dimensional"::: )    ($#l1_collsp :::"CollProjectiveSpace":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "o")) "," (Set (Var "a9")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "FCPS"))  "st" (Bool (Bool (Bool  "not" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "o"))  ($#r1_projdes1 :::"are_coplanar"::: )  )) & (Bool (Set (Var "o")) "," (Set (Var "a")) "," (Set (Var "a9"))  ($#r1_collsp :::"is_collinear"::: )  ) & (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set (Var "a9")))) "holds"  (Bool  "not" (Bool (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "a9"))  ($#r1_projdes1 :::"are_coplanar"::: )  )))) ; 
 
theorem :: PROJDES1:16 (Bool  "for" (Set (Var "FCPS")) "being"   ($#v7_anproj_2 :::"up-3-dimensional"::: )    ($#l1_collsp :::"CollProjectiveSpace":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "a9")) "," (Set (Var "b9")) "," (Set (Var "c9")) "," (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "FCPS"))  "st" (Bool (Bool (Bool  "not" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c"))  ($#r1_collsp :::"is_collinear"::: )  )) & (Bool (Bool  "not" (Set (Var "a9")) "," (Set (Var "b9")) "," (Set (Var "c9"))  ($#r1_collsp :::"is_collinear"::: )  )) & (Bool (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "p"))  ($#r1_projdes1 :::"are_coplanar"::: )  ) & (Bool (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "q"))  ($#r1_projdes1 :::"are_coplanar"::: )  ) & (Bool (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "r"))  ($#r1_projdes1 :::"are_coplanar"::: )  ) & (Bool (Set (Var "a9")) "," (Set (Var "b9")) "," (Set (Var "c9")) "," (Set (Var "p"))  ($#r1_projdes1 :::"are_coplanar"::: )  ) & (Bool (Set (Var "a9")) "," (Set (Var "b9")) "," (Set (Var "c9")) "," (Set (Var "q"))  ($#r1_projdes1 :::"are_coplanar"::: )  ) & (Bool (Set (Var "a9")) "," (Set (Var "b9")) "," (Set (Var "c9")) "," (Set (Var "r"))  ($#r1_projdes1 :::"are_coplanar"::: )  ) & (Bool (Bool  "not" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "a9"))  ($#r1_projdes1 :::"are_coplanar"::: )  ))) "holds"  (Bool (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r"))  ($#r1_collsp :::"is_collinear"::: )  ))) ; 
 
theorem :: PROJDES1:17 (Bool  "for" (Set (Var "FCPS")) "being"   ($#v7_anproj_2 :::"up-3-dimensional"::: )    ($#l1_collsp :::"CollProjectiveSpace":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "a9")) "," (Set (Var "o")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "b9")) "," (Set (Var "c9")) "," (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "FCPS"))  "st" (Bool (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set (Var "a9"))) & (Bool (Set (Var "o")) "," (Set (Var "a")) "," (Set (Var "a9"))  ($#r1_collsp :::"is_collinear"::: )  ) & (Bool (Bool  "not" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "o"))  ($#r1_projdes1 :::"are_coplanar"::: )  )) & (Bool (Bool  "not" (Set (Var "a9")) "," (Set (Var "b9")) "," (Set (Var "c9"))  ($#r1_collsp :::"is_collinear"::: )  )) & (Bool (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "p"))  ($#r1_collsp :::"is_collinear"::: )  ) & (Bool (Set (Var "a9")) "," (Set (Var "b9")) "," (Set (Var "p"))  ($#r1_collsp :::"is_collinear"::: )  ) & (Bool (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "q"))  ($#r1_collsp :::"is_collinear"::: )  ) & (Bool (Set (Var "b9")) "," (Set (Var "c9")) "," (Set (Var "q"))  ($#r1_collsp :::"is_collinear"::: )  ) & (Bool (Set (Var "a")) "," (Set (Var "c")) "," (Set (Var "r"))  ($#r1_collsp :::"is_collinear"::: )  ) & (Bool (Set (Var "a9")) "," (Set (Var "c9")) "," (Set (Var "r"))  ($#r1_collsp :::"is_collinear"::: )  )) "holds"  (Bool (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r"))  ($#r1_collsp :::"is_collinear"::: )  ))) ; 
 
theorem :: PROJDES1:18 (Bool  "for" (Set (Var "FCPS")) "being"   ($#v7_anproj_2 :::"up-3-dimensional"::: )    ($#l1_collsp :::"CollProjectiveSpace":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "o")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "FCPS"))  "st" (Bool (Bool (Bool  "not" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d"))  ($#r1_projdes1 :::"are_coplanar"::: )  )) & (Bool (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "o"))  ($#r1_projdes1 :::"are_coplanar"::: )  ) & (Bool (Bool  "not" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "o"))  ($#r1_collsp :::"is_collinear"::: )  ))) "holds"  (Bool  "not" (Bool (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "d")) "," (Set (Var "o"))  ($#r1_projdes1 :::"are_coplanar"::: )  )))) ; 
 
theorem :: PROJDES1:19 (Bool  "for" (Set (Var "FCPS")) "being"   ($#v7_anproj_2 :::"up-3-dimensional"::: )    ($#l1_collsp :::"CollProjectiveSpace":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "o")) "," (Set (Var "a9")) "," (Set (Var "b9")) "," (Set (Var "c9")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "FCPS"))  "st" (Bool (Bool (Bool  "not" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "o"))  ($#r1_projdes1 :::"are_coplanar"::: )  )) & (Bool (Set (Var "o")) "," (Set (Var "a")) "," (Set (Var "a9"))  ($#r1_collsp :::"is_collinear"::: )  ) & (Bool (Set (Var "o")) "," (Set (Var "b")) "," (Set (Var "b9"))  ($#r1_collsp :::"is_collinear"::: )  ) & (Bool (Set (Var "o")) "," (Set (Var "c")) "," (Set (Var "c9"))  ($#r1_collsp :::"is_collinear"::: )  ) & (Bool (Set (Var "o"))  ($#r1_hidden :::"<>"::: )  (Set (Var "a9"))) & (Bool (Set (Var "o"))  ($#r1_hidden :::"<>"::: )  (Set (Var "b9"))) & (Bool (Set (Var "o"))  ($#r1_hidden :::"<>"::: )  (Set (Var "c9")))) "holds"  (Bool  "("  (Bool (Bool  "not" (Set (Var "a9")) "," (Set (Var "b9")) "," (Set (Var "c9"))  ($#r1_collsp :::"is_collinear"::: )  )) & (Bool (Bool  "not" (Set (Var "a9")) "," (Set (Var "b9")) "," (Set (Var "c9")) "," (Set (Var "o"))  ($#r1_projdes1 :::"are_coplanar"::: )  ))  ")" ))) ; 
 
theorem :: PROJDES1:20 (Bool  "for" (Set (Var "FCPS")) "being"   ($#v7_anproj_2 :::"up-3-dimensional"::: )    ($#l1_collsp :::"CollProjectiveSpace":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "o")) "," (Set (Var "d")) "," (Set (Var "d9")) "," (Set (Var "a9")) "," (Set (Var "b9")) "," (Set (Var "s")) "," (Set (Var "t")) "," (Set (Var "u")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "FCPS"))  "st" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "o"))  ($#r1_projdes1 :::"are_coplanar"::: )  ) & (Bool (Bool  "not" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d"))  ($#r1_projdes1 :::"are_coplanar"::: )  )) & (Bool (Bool  "not" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "d")) "," (Set (Var "o"))  ($#r1_projdes1 :::"are_coplanar"::: )  )) & (Bool (Set (Var "o")) "," (Set (Var "d")) "," (Set (Var "d9"))  ($#r1_collsp :::"is_collinear"::: )  ) & (Bool (Set (Var "o")) "," (Set (Var "a")) "," (Set (Var "a9"))  ($#r1_collsp :::"is_collinear"::: )  ) & (Bool (Set (Var "o")) "," (Set (Var "b")) "," (Set (Var "b9"))  ($#r1_collsp :::"is_collinear"::: )  ) & (Bool (Set (Var "a")) "," (Set (Var "d")) "," (Set (Var "s"))  ($#r1_collsp :::"is_collinear"::: )  ) & (Bool (Set (Var "a9")) "," (Set (Var "d9")) "," (Set (Var "s"))  ($#r1_collsp :::"is_collinear"::: )  ) & (Bool (Set (Var "b")) "," (Set (Var "d")) "," (Set (Var "t"))  ($#r1_collsp :::"is_collinear"::: )  ) & (Bool (Set (Var "b9")) "," (Set (Var "d9")) "," (Set (Var "t"))  ($#r1_collsp :::"is_collinear"::: )  ) & (Bool (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "u"))  ($#r1_collsp :::"is_collinear"::: )  ) & (Bool (Set (Var "o"))  ($#r1_hidden :::"<>"::: )  (Set (Var "a9"))) & (Bool (Set (Var "d"))  ($#r1_hidden :::"<>"::: )  (Set (Var "d9"))) & (Bool (Set (Var "o"))  ($#r1_hidden :::"<>"::: )  (Set (Var "b9")))) "holds"  (Bool  "not" (Bool (Set (Var "s")) "," (Set (Var "t")) "," (Set (Var "u"))  ($#r1_collsp :::"is_collinear"::: )  )))) ; 
 definitionlet "FCPS" be   ($#v7_anproj_2 :::"up-3-dimensional"::: )    ($#l1_collsp :::"CollProjectiveSpace":::); let "o", "a", "b", "c" be   ($#m1_subset_1 :::"Element":::) "of" (Set (Const "FCPS")); pred "o" "," "a" "," "b" "," "c" :::"constitute_a_quadrangle":::  means :: PROJDES1:def 2 (Bool  "("  (Bool (Bool  "not" "a" "," "b" "," "c"  ($#r1_collsp :::"is_collinear"::: )  )) & (Bool (Bool  "not" "o" "," "a" "," "b"  ($#r1_collsp :::"is_collinear"::: )  )) & (Bool (Bool  "not" "o" "," "b" "," "c"  ($#r1_collsp :::"is_collinear"::: )  )) & (Bool (Bool  "not" "o" "," "c" "," "a"  ($#r1_collsp :::"is_collinear"::: )  ))  ")" ); end; 








:: deftheorem    defines :::"constitute_a_quadrangle"::: PROJDES1:def 2 :  (Bool  "for" (Set (Var "FCPS")) "being"   ($#v7_anproj_2 :::"up-3-dimensional"::: )    ($#l1_collsp :::"CollProjectiveSpace":::)  (Bool  "for" (Set (Var "o")) "," (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "FCPS")) "holds"   (Bool  "("  (Bool (Set (Var "o")) "," (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c"))  ($#r2_projdes1 :::"constitute_a_quadrangle"::: )  ) "iff" (Bool  "("  (Bool (Bool  "not" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c"))  ($#r1_collsp :::"is_collinear"::: )  )) & (Bool (Bool  "not" (Set (Var "o")) "," (Set (Var "a")) "," (Set (Var "b"))  ($#r1_collsp :::"is_collinear"::: )  )) & (Bool (Bool  "not" (Set (Var "o")) "," (Set (Var "b")) "," (Set (Var "c"))  ($#r1_collsp :::"is_collinear"::: )  )) & (Bool (Bool  "not" (Set (Var "o")) "," (Set (Var "c")) "," (Set (Var "a"))  ($#r1_collsp :::"is_collinear"::: )  ))  ")" )  ")" ))); 
 
theorem :: PROJDES1:21 (Bool  "for" (Set (Var "FCPS")) "being"   ($#v7_anproj_2 :::"up-3-dimensional"::: )    ($#l1_collsp :::"CollProjectiveSpace":::)  (Bool  "for" (Set (Var "o")) "," (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "a9")) "," (Set (Var "b9")) "," (Set (Var "c9")) "," (Set (Var "p")) "," (Set (Var "r")) "," (Set (Var "q")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "FCPS"))  "st" (Bool (Bool (Bool  "not" (Set (Var "o")) "," (Set (Var "a")) "," (Set (Var "b"))  ($#r1_collsp :::"is_collinear"::: )  )) & (Bool (Bool  "not" (Set (Var "o")) "," (Set (Var "b")) "," (Set (Var "c"))  ($#r1_collsp :::"is_collinear"::: )  )) & (Bool (Bool  "not" (Set (Var "o")) "," (Set (Var "a")) "," (Set (Var "c"))  ($#r1_collsp :::"is_collinear"::: )  )) & (Bool (Set (Var "o")) "," (Set (Var "a")) "," (Set (Var "a9"))  ($#r1_collsp :::"is_collinear"::: )  ) & (Bool (Set (Var "o")) "," (Set (Var "b")) "," (Set (Var "b9"))  ($#r1_collsp :::"is_collinear"::: )  ) & (Bool (Set (Var "o")) "," (Set (Var "c")) "," (Set (Var "c9"))  ($#r1_collsp :::"is_collinear"::: )  ) & (Bool (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "p"))  ($#r1_collsp :::"is_collinear"::: )  ) & (Bool (Set (Var "a9")) "," (Set (Var "b9")) "," (Set (Var "p"))  ($#r1_collsp :::"is_collinear"::: )  ) & (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set (Var "a9"))) & (Bool (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "r"))  ($#r1_collsp :::"is_collinear"::: )  ) & (Bool (Set (Var "b9")) "," (Set (Var "c9")) "," (Set (Var "r"))  ($#r1_collsp :::"is_collinear"::: )  ) & (Bool (Set (Var "a")) "," (Set (Var "c")) "," (Set (Var "q"))  ($#r1_collsp :::"is_collinear"::: )  ) & (Bool (Set (Var "b"))  ($#r1_hidden :::"<>"::: )  (Set (Var "b9"))) & (Bool (Set (Var "a9")) "," (Set (Var "c9")) "," (Set (Var "q"))  ($#r1_collsp :::"is_collinear"::: )  ) & (Bool (Set (Var "o"))  ($#r1_hidden :::"<>"::: )  (Set (Var "a9"))) & (Bool (Set (Var "o"))  ($#r1_hidden :::"<>"::: )  (Set (Var "b9"))) & (Bool (Set (Var "o"))  ($#r1_hidden :::"<>"::: )  (Set (Var "c9")))) "holds"  (Bool (Set (Var "r")) "," (Set (Var "q")) "," (Set (Var "p"))  ($#r1_collsp :::"is_collinear"::: )  ))) ; 
 
theorem :: PROJDES1:22 (Bool  "for" (Set (Var "CS")) "being"   ($#v7_anproj_2 :::"up-3-dimensional"::: )    ($#l1_collsp :::"CollProjectiveSpace":::) "holds"  (Bool (Set (Var "CS")) "is"   ($#v5_anproj_2 :::"Desarguesian"::: )  )) ; 
 registration
cluster bbbadV2_STRUCT_0() bbbadV2_COLLSP() bbbadV3_COLLSP()   ($#v4_collsp :::"proper"::: )     ($#v2_anproj_2 :::"Vebleian"::: )     ($#v3_anproj_2 :::"at_least_3rank"::: )     ($#v7_anproj_2 :::"up-3-dimensional"::: )    ->   ($#v5_anproj_2 :::"Desarguesian"::: )     ($#v7_anproj_2 :::"up-3-dimensional"::: )    for  bbbadL1_COLLSP(); 
end;