:: HESSENBE  semantic presentation begin  
































theorem :: HESSENBE:1 (Bool  "for" (Set (Var "PCPP")) "being"   ($#l1_collsp :::"CollProjectiveSpace":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "PCPP"))  "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 :: HESSENBE:2 (Bool  "for" (Set (Var "PCPP")) "being"   ($#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 "PCPP"))  "st" (Bool (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set (Var "b"))) & (Bool (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"::: )  )) "holds"  (Bool (Set (Var "a")) "," (Set (Var "c")) "," (Set (Var "d"))  ($#r1_collsp :::"is_collinear"::: )  ))) ; 
 
theorem :: HESSENBE:3 (Bool  "for" (Set (Var "PCPP")) "being"   ($#l1_collsp :::"CollProjectiveSpace":::)  (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "r")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "PCPP"))  "st" (Bool (Bool (Set (Var "p"))  ($#r1_hidden :::"<>"::: )  (Set (Var "q"))) & (Bool (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "p"))  ($#r1_collsp :::"is_collinear"::: )  ) & (Bool (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "q"))  ($#r1_collsp :::"is_collinear"::: )  ) & (Bool (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r"))  ($#r1_collsp :::"is_collinear"::: )  )) "holds"  (Bool (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "r"))  ($#r1_collsp :::"is_collinear"::: )  ))) ; 
 
theorem :: HESSENBE:4 (Bool  "for" (Set (Var "PCPP")) "being"   ($#l1_collsp :::"CollProjectiveSpace":::)  (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "PCPP"))  "st" (Bool (Bool (Set (Var "p"))  ($#r1_hidden :::"<>"::: )  (Set (Var "q")))) "holds"  (Bool  "ex" (Set (Var "r")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "PCPP")) "st" (Bool (Bool  "not" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r"))  ($#r1_collsp :::"is_collinear"::: )  ))))) ; 
 
theorem :: HESSENBE:5 (Bool  "for" (Set (Var "PCPP")) "being"   ($#l1_collsp :::"CollProjectiveSpace":::)  (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "PCPP"))  "holds"  (Bool  "not" (Bool  "for" (Set (Var "q")) "," (Set (Var "r")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "PCPP")) "holds"  (Bool (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r"))  ($#r1_collsp :::"is_collinear"::: )  ))))) ; 
 
theorem :: HESSENBE:6 (Bool  "for" (Set (Var "PCPP")) "being"   ($#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 "PCPP"))  "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 :: HESSENBE:7 (Bool  "for" (Set (Var "PCPP")) "being"   ($#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 "PCPP"))  "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 :: HESSENBE:8 (Bool  "for" (Set (Var "PCPP")) "being"   ($#l1_collsp :::"CollProjectiveSpace":::)  (Bool  "for" (Set (Var "o")) "," (Set (Var "a")) "," (Set (Var "d")) "," (Set (Var "d9")) "," (Set (Var "a9")) "," (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "PCPP"))  "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 "x"))  ($#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 "x"))  ($#r1_hidden :::"<>"::: )  (Set (Var "d"))))) ; 
 
theorem :: HESSENBE:9 (Bool  "for" (Set (Var "PCPP")) "being"   ($#l1_collsp :::"CollProjectiveSpace":::)  (Bool  "for" (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) "," (Set (Var "c3")) "," (Set (Var "c1")) "," (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "PCPP"))  "st" (Bool (Bool (Bool  "not" (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3"))  ($#r1_collsp :::"is_collinear"::: )  )) & (Bool (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "c3"))  ($#r1_collsp :::"is_collinear"::: )  ) & (Bool (Set (Var "a2")) "," (Set (Var "a3")) "," (Set (Var "c1"))  ($#r1_collsp :::"is_collinear"::: )  ) & (Bool (Set (Var "c1")) "," (Set (Var "c3")) "," (Set (Var "x"))  ($#r1_collsp :::"is_collinear"::: )  ) & (Bool (Set (Var "c3"))  ($#r1_hidden :::"<>"::: )  (Set (Var "a1"))) & (Bool (Set (Var "c3"))  ($#r1_hidden :::"<>"::: )  (Set (Var "a2"))) & (Bool (Set (Var "c1"))  ($#r1_hidden :::"<>"::: )  (Set (Var "a2"))) & (Bool (Set (Var "c1"))  ($#r1_hidden :::"<>"::: )  (Set (Var "a3")))) "holds"  (Bool  "("  (Bool (Set (Var "a1"))  ($#r1_hidden :::"<>"::: )  (Set (Var "x"))) & (Bool (Set (Var "a3"))  ($#r1_hidden :::"<>"::: )  (Set (Var "x")))  ")" ))) ; 
 
theorem :: HESSENBE:10 (Bool  "for" (Set (Var "PCPP")) "being"   ($#l1_collsp :::"CollProjectiveSpace":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "e")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "PCPP"))  "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 "c")) "," (Set (Var "e")) "," (Set (Var "d"))  ($#r1_collsp :::"is_collinear"::: )  ) & (Bool (Set (Var "e"))  ($#r1_hidden :::"<>"::: )  (Set (Var "c"))) & (Bool (Set (Var "d"))  ($#r1_hidden :::"<>"::: )  (Set (Var "a")))) "holds"  (Bool  "not" (Bool (Set (Var "e")) "," (Set (Var "a")) "," (Set (Var "c"))  ($#r1_collsp :::"is_collinear"::: )  )))) ; 
 
theorem :: HESSENBE:11 (Bool  "for" (Set (Var "PCPP")) "being"   ($#l1_collsp :::"CollProjectiveSpace":::)  (Bool  "for" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "q1")) "," (Set (Var "q2")) "," (Set (Var "q3")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "PCPP"))  "st" (Bool (Bool (Bool  "not" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "q1"))  ($#r1_collsp :::"is_collinear"::: )  )) & (Bool (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "q2"))  ($#r1_collsp :::"is_collinear"::: )  ) & (Bool (Set (Var "q1")) "," (Set (Var "q2")) "," (Set (Var "q3"))  ($#r1_collsp :::"is_collinear"::: )  ) & (Bool (Set (Var "q2"))  ($#r1_hidden :::"<>"::: )  (Set (Var "q3")))) "holds"  (Bool  "not" (Bool (Set (Var "p2")) "," (Set (Var "p1")) "," (Set (Var "q3"))  ($#r1_collsp :::"is_collinear"::: )  )))) ; 
 
theorem :: HESSENBE:12 (Bool  "for" (Set (Var "PCPP")) "being"   ($#l1_collsp :::"CollProjectiveSpace":::)  (Bool  "for" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "q1")) "," (Set (Var "p3")) "," (Set (Var "q2")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "PCPP"))  "st" (Bool (Bool (Bool  "not" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "q1"))  ($#r1_collsp :::"is_collinear"::: )  )) & (Bool (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p3"))  ($#r1_collsp :::"is_collinear"::: )  ) & (Bool (Set (Var "q1")) "," (Set (Var "q2")) "," (Set (Var "p3"))  ($#r1_collsp :::"is_collinear"::: )  ) & (Bool (Set (Var "p3"))  ($#r1_hidden :::"<>"::: )  (Set (Var "q2"))) & (Bool (Set (Var "p2"))  ($#r1_hidden :::"<>"::: )  (Set (Var "p3")))) "holds"  (Bool  "not" (Bool (Set (Var "p3")) "," (Set (Var "p2")) "," (Set (Var "q2"))  ($#r1_collsp :::"is_collinear"::: )  )))) ; 
 
theorem :: HESSENBE:13 (Bool  "for" (Set (Var "PCPP")) "being"   ($#l1_collsp :::"CollProjectiveSpace":::)  (Bool  "for" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "q1")) "," (Set (Var "p3")) "," (Set (Var "q2")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "PCPP"))  "st" (Bool (Bool (Bool  "not" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "q1"))  ($#r1_collsp :::"is_collinear"::: )  )) & (Bool (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p3"))  ($#r1_collsp :::"is_collinear"::: )  ) & (Bool (Set (Var "q1")) "," (Set (Var "q2")) "," (Set (Var "p1"))  ($#r1_collsp :::"is_collinear"::: )  ) & (Bool (Set (Var "p1"))  ($#r1_hidden :::"<>"::: )  (Set (Var "p3"))) & (Bool (Set (Var "p1"))  ($#r1_hidden :::"<>"::: )  (Set (Var "q2")))) "holds"  (Bool  "not" (Bool (Set (Var "p3")) "," (Set (Var "p1")) "," (Set (Var "q2"))  ($#r1_collsp :::"is_collinear"::: )  )))) ; 
 
theorem :: HESSENBE:14 (Bool  "for" (Set (Var "PCPP")) "being"   ($#l1_collsp :::"CollProjectiveSpace":::)  (Bool  "for" (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "b1")) "," (Set (Var "b2")) "," (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "PCPP"))  "st" (Bool (Bool (Set (Var "a1"))  ($#r1_hidden :::"<>"::: )  (Set (Var "a2"))) & (Bool (Set (Var "b1"))  ($#r1_hidden :::"<>"::: )  (Set (Var "b2"))) & (Bool (Set (Var "b1")) "," (Set (Var "b2")) "," (Set (Var "x"))  ($#r1_collsp :::"is_collinear"::: )  ) & (Bool (Set (Var "b1")) "," (Set (Var "b2")) "," (Set (Var "y"))  ($#r1_collsp :::"is_collinear"::: )  ) & (Bool (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "x"))  ($#r1_collsp :::"is_collinear"::: )  ) & (Bool (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "y"))  ($#r1_collsp :::"is_collinear"::: )  ) & (Bool (Bool  "not" (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "b1"))  ($#r1_collsp :::"is_collinear"::: )  ))) "holds"  (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set (Var "y"))))) ; 
 
theorem :: HESSENBE:15 (Bool  "for" (Set (Var "PCPP")) "being"   ($#l1_collsp :::"CollProjectiveSpace":::)  (Bool  "for" (Set (Var "o")) "," (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "b1")) "," (Set (Var "b2")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "PCPP"))  "st" (Bool (Bool (Bool  "not" (Set (Var "o")) "," (Set (Var "a1")) "," (Set (Var "a2"))  ($#r1_collsp :::"is_collinear"::: )  )) & (Bool (Set (Var "o")) "," (Set (Var "a1")) "," (Set (Var "b1"))  ($#r1_collsp :::"is_collinear"::: )  ) & (Bool (Set (Var "o")) "," (Set (Var "a2")) "," (Set (Var "b2"))  ($#r1_collsp :::"is_collinear"::: )  ) & (Bool (Set (Var "o"))  ($#r1_hidden :::"<>"::: )  (Set (Var "b1"))) & (Bool (Set (Var "o"))  ($#r1_hidden :::"<>"::: )  (Set (Var "b2")))) "holds"  (Bool  "not" (Bool (Set (Var "o")) "," (Set (Var "b1")) "," (Set (Var "b2"))  ($#r1_collsp :::"is_collinear"::: )  )))) ; 
 
































theorem :: HESSENBE:16 (Bool  "for" (Set (Var "PCPP")) "being"   ($#v6_anproj_2 :::"Pappian"::: )    ($#l1_collsp :::"CollProjectivePlane":::)  (Bool  "for" (Set (Var "p2")) "," (Set (Var "p3")) "," (Set (Var "p1")) "," (Set (Var "q2")) "," (Set (Var "q3")) "," (Set (Var "q1")) "," (Set (Var "r3")) "," (Set (Var "r2")) "," (Set (Var "r1")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "PCPP"))  "st" (Bool (Bool (Set (Var "p2"))  ($#r1_hidden :::"<>"::: )  (Set (Var "p3"))) & (Bool (Set (Var "p1"))  ($#r1_hidden :::"<>"::: )  (Set (Var "p3"))) & (Bool (Set (Var "q2"))  ($#r1_hidden :::"<>"::: )  (Set (Var "q3"))) & (Bool (Set (Var "q1"))  ($#r1_hidden :::"<>"::: )  (Set (Var "q2"))) & (Bool (Set (Var "q1"))  ($#r1_hidden :::"<>"::: )  (Set (Var "q3"))) & (Bool (Bool  "not" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "q1"))  ($#r1_collsp :::"is_collinear"::: )  )) & (Bool (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p3"))  ($#r1_collsp :::"is_collinear"::: )  ) & (Bool (Set (Var "q1")) "," (Set (Var "q2")) "," (Set (Var "q3"))  ($#r1_collsp :::"is_collinear"::: )  ) & (Bool (Set (Var "p1")) "," (Set (Var "q2")) "," (Set (Var "r3"))  ($#r1_collsp :::"is_collinear"::: )  ) & (Bool (Set (Var "q1")) "," (Set (Var "p2")) "," (Set (Var "r3"))  ($#r1_collsp :::"is_collinear"::: )  ) & (Bool (Set (Var "p1")) "," (Set (Var "q3")) "," (Set (Var "r2"))  ($#r1_collsp :::"is_collinear"::: )  ) & (Bool (Set (Var "p3")) "," (Set (Var "q1")) "," (Set (Var "r2"))  ($#r1_collsp :::"is_collinear"::: )  ) & (Bool (Set (Var "p2")) "," (Set (Var "q3")) "," (Set (Var "r1"))  ($#r1_collsp :::"is_collinear"::: )  ) & (Bool (Set (Var "p3")) "," (Set (Var "q2")) "," (Set (Var "r1"))  ($#r1_collsp :::"is_collinear"::: )  )) "holds"  (Bool (Set (Var "r1")) "," (Set (Var "r2")) "," (Set (Var "r3"))  ($#r1_collsp :::"is_collinear"::: )  ))) ; 
 
theorem :: HESSENBE:17 (Bool  "for" (Set (Var "PCPP")) "being"   ($#v6_anproj_2 :::"Pappian"::: )    ($#l1_collsp :::"CollProjectivePlane":::)  (Bool  "for" (Set (Var "o")) "," (Set (Var "b1")) "," (Set (Var "a1")) "," (Set (Var "b2")) "," (Set (Var "a2")) "," (Set (Var "b3")) "," (Set (Var "a3")) "," (Set (Var "c3")) "," (Set (Var "c1")) "," (Set (Var "c2")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "PCPP"))  "st" (Bool (Bool (Set (Var "o"))  ($#r1_hidden :::"<>"::: )  (Set (Var "b1"))) & (Bool (Set (Var "a1"))  ($#r1_hidden :::"<>"::: )  (Set (Var "b1"))) & (Bool (Set (Var "o"))  ($#r1_hidden :::"<>"::: )  (Set (Var "b2"))) & (Bool (Set (Var "a2"))  ($#r1_hidden :::"<>"::: )  (Set (Var "b2"))) & (Bool (Set (Var "o"))  ($#r1_hidden :::"<>"::: )  (Set (Var "b3"))) & (Bool (Set (Var "a3"))  ($#r1_hidden :::"<>"::: )  (Set (Var "b3"))) & (Bool (Bool  "not" (Set (Var "o")) "," (Set (Var "a1")) "," (Set (Var "a2"))  ($#r1_collsp :::"is_collinear"::: )  )) & (Bool (Bool  "not" (Set (Var "o")) "," (Set (Var "a1")) "," (Set (Var "a3"))  ($#r1_collsp :::"is_collinear"::: )  )) & (Bool (Bool  "not" (Set (Var "o")) "," (Set (Var "a2")) "," (Set (Var "a3"))  ($#r1_collsp :::"is_collinear"::: )  )) & (Bool (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "c3"))  ($#r1_collsp :::"is_collinear"::: )  ) & (Bool (Set (Var "b1")) "," (Set (Var "b2")) "," (Set (Var "c3"))  ($#r1_collsp :::"is_collinear"::: )  ) & (Bool (Set (Var "a2")) "," (Set (Var "a3")) "," (Set (Var "c1"))  ($#r1_collsp :::"is_collinear"::: )  ) & (Bool (Set (Var "b2")) "," (Set (Var "b3")) "," (Set (Var "c1"))  ($#r1_collsp :::"is_collinear"::: )  ) & (Bool (Set (Var "a1")) "," (Set (Var "a3")) "," (Set (Var "c2"))  ($#r1_collsp :::"is_collinear"::: )  ) & (Bool (Set (Var "b1")) "," (Set (Var "b3")) "," (Set (Var "c2"))  ($#r1_collsp :::"is_collinear"::: )  ) & (Bool (Set (Var "o")) "," (Set (Var "a1")) "," (Set (Var "b1"))  ($#r1_collsp :::"is_collinear"::: )  ) & (Bool (Set (Var "o")) "," (Set (Var "a2")) "," (Set (Var "b2"))  ($#r1_collsp :::"is_collinear"::: )  ) & (Bool (Set (Var "o")) "," (Set (Var "a3")) "," (Set (Var "b3"))  ($#r1_collsp :::"is_collinear"::: )  )) "holds"  (Bool (Set (Var "c1")) "," (Set (Var "c2")) "," (Set (Var "c3"))  ($#r1_collsp :::"is_collinear"::: )  ))) ; 
 registration
cluster bbbadV2_STRUCT_0() bbbadV2_COLLSP() bbbadV3_COLLSP()   ($#v4_collsp :::"proper"::: )     ($#v2_anproj_2 :::"Vebleian"::: )     ($#v3_anproj_2 :::"at_least_3rank"::: )     ($#v6_anproj_2 :::"Pappian"::: )    ->   ($#v5_anproj_2 :::"Desarguesian"::: )    for  bbbadL1_COLLSP(); 
end;