:: PARSP_2  semantic presentation begin  



theorem :: PARSP_2:1 (Bool  "for" (Set (Var "F")) "being"   ($#l6_algstr_0 :::"Field":::) "holds"  (Bool (Set   ($#k9_parsp_1 :::"MPS"::: )  (Set (Var "F"))) "is"   ($#l1_parsp_1 :::"ParSp":::))) ; 
 































theorem :: PARSP_2:2 (Bool  "for" (Set (Var "F")) "being"   ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set  "("  ($#k9_parsp_1 :::"MPS"::: )  (Set (Var "F")) ")" ) "holds"   (Bool  "("  (Bool (Set (Var "a")) "," (Set (Var "b"))  ($#r1_parsp_1 :::"'||'"::: )  (Set (Var "c")) "," (Set (Var "d"))) "iff" (Bool  "ex" (Set (Var "e")) "," (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "h")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set  ($#k3_zfmisc_1 :::"[:"::: ) (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "F"))) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "F"))) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "F"))) ($#k3_zfmisc_1 :::":]"::: ) ) "st"  (Bool  "("  (Bool (Set  ($#k5_domain_1 :::"["::: ) (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) ($#k5_domain_1 :::"]"::: ) )  ($#r1_hidden :::"="::: )  (Set  ($#k6_xtuple_0 :::"["::: ) (Set (Var "e")) "," (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "h")) ($#k6_xtuple_0 :::"]"::: ) )) & (Bool  "("  (Bool  "ex" (Set (Var "K")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "F")) "st"  (Bool  "("  (Bool (Set (Set (Var "K"))  ($#k8_group_1 :::"*"::: )  (Set  "(" (Set  "(" (Set (Var "e"))  ($#k1_mcart_1 :::"`1_3"::: )  ")" )  ($#k5_algstr_0 :::"-"::: )  (Set  "(" (Set (Var "f"))  ($#k1_mcart_1 :::"`1_3"::: )  ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "g"))  ($#k1_mcart_1 :::"`1_3"::: )  ")" )  ($#k5_algstr_0 :::"-"::: )  (Set  "(" (Set (Var "h"))  ($#k1_mcart_1 :::"`1_3"::: )  ")" ))) & (Bool (Set (Set (Var "K"))  ($#k8_group_1 :::"*"::: )  (Set  "(" (Set  "(" (Set (Var "e"))  ($#k2_mcart_1 :::"`2_3"::: )  ")" )  ($#k5_algstr_0 :::"-"::: )  (Set  "(" (Set (Var "f"))  ($#k2_mcart_1 :::"`2_3"::: )  ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "g"))  ($#k2_mcart_1 :::"`2_3"::: )  ")" )  ($#k5_algstr_0 :::"-"::: )  (Set  "(" (Set (Var "h"))  ($#k2_mcart_1 :::"`2_3"::: )  ")" ))) & (Bool (Set (Set (Var "K"))  ($#k8_group_1 :::"*"::: )  (Set  "(" (Set  "(" (Set (Var "e"))  ($#k3_mcart_1 :::"`3_3"::: )  ")" )  ($#k5_algstr_0 :::"-"::: )  (Set  "(" (Set (Var "f"))  ($#k3_mcart_1 :::"`3_3"::: )  ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "g"))  ($#k3_mcart_1 :::"`3_3"::: )  ")" )  ($#k5_algstr_0 :::"-"::: )  (Set  "(" (Set (Var "h"))  ($#k3_mcart_1 :::"`3_3"::: )  ")" )))  ")" )) "or" (Bool  "("  (Bool (Set (Set  "(" (Set (Var "e"))  ($#k1_mcart_1 :::"`1_3"::: )  ")" )  ($#k5_algstr_0 :::"-"::: )  (Set  "(" (Set (Var "f"))  ($#k1_mcart_1 :::"`1_3"::: )  ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k4_struct_0 :::"0."::: )  (Set (Var "F")))) & (Bool (Set (Set  "(" (Set (Var "e"))  ($#k2_mcart_1 :::"`2_3"::: )  ")" )  ($#k5_algstr_0 :::"-"::: )  (Set  "(" (Set (Var "f"))  ($#k2_mcart_1 :::"`2_3"::: )  ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k4_struct_0 :::"0."::: )  (Set (Var "F")))) & (Bool (Set (Set  "(" (Set (Var "e"))  ($#k3_mcart_1 :::"`3_3"::: )  ")" )  ($#k5_algstr_0 :::"-"::: )  (Set  "(" (Set (Var "f"))  ($#k3_mcart_1 :::"`3_3"::: )  ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k4_struct_0 :::"0."::: )  (Set (Var "F"))))  ")" )  ")" )  ")" ))  ")" ))) ; 
 
theorem :: PARSP_2:3 (Bool  "for" (Set (Var "F")) "being"   ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set  "("  ($#k9_parsp_1 :::"MPS"::: )  (Set (Var "F")) ")" )  (Bool  "for" (Set (Var "e")) "," (Set (Var "f")) "," (Set (Var "g")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set  ($#k3_zfmisc_1 :::"[:"::: ) (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "F"))) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "F"))) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "F"))) ($#k3_zfmisc_1 :::":]"::: ) )  "st" (Bool (Bool (Bool  "not" (Set (Var "a")) "," (Set (Var "b"))  ($#r1_parsp_1 :::"'||'"::: )  (Set (Var "a")) "," (Set (Var "c")))) & (Bool (Set  ($#k5_domain_1 :::"["::: ) (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "a")) "," (Set (Var "c")) ($#k5_domain_1 :::"]"::: ) )  ($#r1_hidden :::"="::: )  (Set  ($#k6_xtuple_0 :::"["::: ) (Set (Var "e")) "," (Set (Var "f")) "," (Set (Var "e")) "," (Set (Var "g")) ($#k6_xtuple_0 :::"]"::: ) ))) "holds"  (Bool  "("  (Bool (Set (Var "e"))  ($#r1_hidden :::"<>"::: )  (Set (Var "f"))) & (Bool (Set (Var "e"))  ($#r1_hidden :::"<>"::: )  (Set (Var "g"))) & (Bool (Set (Var "f"))  ($#r1_hidden :::"<>"::: )  (Set (Var "g")))  ")" )))) ; 
 
theorem :: PARSP_2:4 (Bool  "for" (Set (Var "F")) "being"   ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set  "("  ($#k9_parsp_1 :::"MPS"::: )  (Set (Var "F")) ")" )  (Bool  "for" (Set (Var "e")) "," (Set (Var "f")) "," (Set (Var "g")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set  ($#k3_zfmisc_1 :::"[:"::: ) (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "F"))) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "F"))) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "F"))) ($#k3_zfmisc_1 :::":]"::: ) )  (Bool  "for" (Set (Var "K")) "," (Set (Var "L")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "F"))  "st" (Bool (Bool (Bool  "not" (Set (Var "a")) "," (Set (Var "b"))  ($#r1_parsp_1 :::"'||'"::: )  (Set (Var "a")) "," (Set (Var "c")))) & (Bool (Set  ($#k5_domain_1 :::"["::: ) (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "a")) "," (Set (Var "c")) ($#k5_domain_1 :::"]"::: ) )  ($#r1_hidden :::"="::: )  (Set  ($#k6_xtuple_0 :::"["::: ) (Set (Var "e")) "," (Set (Var "f")) "," (Set (Var "e")) "," (Set (Var "g")) ($#k6_xtuple_0 :::"]"::: ) )) & (Bool (Set (Set (Var "K"))  ($#k8_group_1 :::"*"::: )  (Set  "(" (Set  "(" (Set (Var "e"))  ($#k1_mcart_1 :::"`1_3"::: )  ")" )  ($#k5_algstr_0 :::"-"::: )  (Set  "(" (Set (Var "f"))  ($#k1_mcart_1 :::"`1_3"::: )  ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "L"))  ($#k8_group_1 :::"*"::: )  (Set  "(" (Set  "(" (Set (Var "e"))  ($#k1_mcart_1 :::"`1_3"::: )  ")" )  ($#k5_algstr_0 :::"-"::: )  (Set  "(" (Set (Var "g"))  ($#k1_mcart_1 :::"`1_3"::: )  ")" ) ")" ))) & (Bool (Set (Set (Var "K"))  ($#k8_group_1 :::"*"::: )  (Set  "(" (Set  "(" (Set (Var "e"))  ($#k2_mcart_1 :::"`2_3"::: )  ")" )  ($#k5_algstr_0 :::"-"::: )  (Set  "(" (Set (Var "f"))  ($#k2_mcart_1 :::"`2_3"::: )  ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "L"))  ($#k8_group_1 :::"*"::: )  (Set  "(" (Set  "(" (Set (Var "e"))  ($#k2_mcart_1 :::"`2_3"::: )  ")" )  ($#k5_algstr_0 :::"-"::: )  (Set  "(" (Set (Var "g"))  ($#k2_mcart_1 :::"`2_3"::: )  ")" ) ")" ))) & (Bool (Set (Set (Var "K"))  ($#k8_group_1 :::"*"::: )  (Set  "(" (Set  "(" (Set (Var "e"))  ($#k3_mcart_1 :::"`3_3"::: )  ")" )  ($#k5_algstr_0 :::"-"::: )  (Set  "(" (Set (Var "f"))  ($#k3_mcart_1 :::"`3_3"::: )  ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "L"))  ($#k8_group_1 :::"*"::: )  (Set  "(" (Set  "(" (Set (Var "e"))  ($#k3_mcart_1 :::"`3_3"::: )  ")" )  ($#k5_algstr_0 :::"-"::: )  (Set  "(" (Set (Var "g"))  ($#k3_mcart_1 :::"`3_3"::: )  ")" ) ")" )))) "holds"  (Bool  "("  (Bool (Set (Var "K"))  ($#r1_hidden :::"="::: )  (Set   ($#k4_struct_0 :::"0."::: )  (Set (Var "F")))) & (Bool (Set (Var "L"))  ($#r1_hidden :::"="::: )  (Set   ($#k4_struct_0 :::"0."::: )  (Set (Var "F"))))  ")" ))))) ; 
 
theorem :: PARSP_2:5 (Bool  "for" (Set (Var "F")) "being"   ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set  "("  ($#k9_parsp_1 :::"MPS"::: )  (Set (Var "F")) ")" )  (Bool  "for" (Set (Var "e")) "," (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "h")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set  ($#k3_zfmisc_1 :::"[:"::: ) (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "F"))) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "F"))) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "F"))) ($#k3_zfmisc_1 :::":]"::: ) )  "st" (Bool (Bool (Bool  "not" (Set (Var "a")) "," (Set (Var "b"))  ($#r1_parsp_1 :::"'||'"::: )  (Set (Var "a")) "," (Set (Var "c")))) & (Bool (Set (Var "a")) "," (Set (Var "b"))  ($#r1_parsp_1 :::"'||'"::: )  (Set (Var "c")) "," (Set (Var "d"))) & (Bool (Set (Var "a")) "," (Set (Var "c"))  ($#r1_parsp_1 :::"'||'"::: )  (Set (Var "b")) "," (Set (Var "d"))) & (Bool (Set  ($#k5_domain_1 :::"["::: ) (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) ($#k5_domain_1 :::"]"::: ) )  ($#r1_hidden :::"="::: )  (Set  ($#k6_xtuple_0 :::"["::: ) (Set (Var "e")) "," (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "h")) ($#k6_xtuple_0 :::"]"::: ) ))) "holds"  (Bool  "("  (Bool (Set (Set (Var "h"))  ($#k1_mcart_1 :::"`1_3"::: )  )  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set (Var "f"))  ($#k1_mcart_1 :::"`1_3"::: )  ")" )  ($#k3_rlvect_1 :::"+"::: )  (Set  "(" (Set (Var "g"))  ($#k1_mcart_1 :::"`1_3"::: )  ")" ) ")" )  ($#k5_algstr_0 :::"-"::: )  (Set  "(" (Set (Var "e"))  ($#k1_mcart_1 :::"`1_3"::: )  ")" ))) & (Bool (Set (Set (Var "h"))  ($#k2_mcart_1 :::"`2_3"::: )  )  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set (Var "f"))  ($#k2_mcart_1 :::"`2_3"::: )  ")" )  ($#k3_rlvect_1 :::"+"::: )  (Set  "(" (Set (Var "g"))  ($#k2_mcart_1 :::"`2_3"::: )  ")" ) ")" )  ($#k5_algstr_0 :::"-"::: )  (Set  "(" (Set (Var "e"))  ($#k2_mcart_1 :::"`2_3"::: )  ")" ))) & (Bool (Set (Set (Var "h"))  ($#k3_mcart_1 :::"`3_3"::: )  )  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set (Var "f"))  ($#k3_mcart_1 :::"`3_3"::: )  ")" )  ($#k3_rlvect_1 :::"+"::: )  (Set  "(" (Set (Var "g"))  ($#k3_mcart_1 :::"`3_3"::: )  ")" ) ")" )  ($#k5_algstr_0 :::"-"::: )  (Set  "(" (Set (Var "e"))  ($#k3_mcart_1 :::"`3_3"::: )  ")" )))  ")" )))) ; 
 
theorem :: PARSP_2:6 (Bool  "for" (Set (Var "F")) "being"   ($#l6_algstr_0 :::"Field":::)  "holds"  (Bool  "not" (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set  "("  ($#k9_parsp_1 :::"MPS"::: )  (Set (Var "F")) ")" ) "holds"  (Bool (Set (Var "a")) "," (Set (Var "b"))  ($#r1_parsp_1 :::"'||'"::: )  (Set (Var "a")) "," (Set (Var "c")))))) ; 
 
theorem :: PARSP_2:7 (Bool  "for" (Set (Var "F")) "being"   ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "a")) "," (Set (Var "d")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set  "("  ($#k9_parsp_1 :::"MPS"::: )  (Set (Var "F")) ")" )  "st" (Bool (Bool (Set (Set  "("  ($#k1_group_1 :::"1_"::: )  (Set (Var "F")) ")" )  ($#k3_rlvect_1 :::"+"::: )  (Set  "("  ($#k1_group_1 :::"1_"::: )  (Set (Var "F")) ")" ))  ($#r1_hidden :::"<>"::: )  (Set   ($#k4_struct_0 :::"0."::: )  (Set (Var "F")))) & (Bool (Set (Var "b")) "," (Set (Var "c"))  ($#r1_parsp_1 :::"'||'"::: )  (Set (Var "a")) "," (Set (Var "d"))) & (Bool (Set (Var "a")) "," (Set (Var "b"))  ($#r1_parsp_1 :::"'||'"::: )  (Set (Var "c")) "," (Set (Var "d"))) & (Bool (Set (Var "a")) "," (Set (Var "c"))  ($#r1_parsp_1 :::"'||'"::: )  (Set (Var "b")) "," (Set (Var "d")))) "holds"  (Bool (Set (Var "a")) "," (Set (Var "b"))  ($#r1_parsp_1 :::"'||'"::: )  (Set (Var "a")) "," (Set (Var "c"))))) ; 
 
theorem :: PARSP_2:8 (Bool  "for" (Set (Var "F")) "being"   ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "p")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "q")) "," (Set (Var "r")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set  "("  ($#k9_parsp_1 :::"MPS"::: )  (Set (Var "F")) ")" )  "st" (Bool (Bool (Bool  "not" (Set (Var "a")) "," (Set (Var "p"))  ($#r1_parsp_1 :::"'||'"::: )  (Set (Var "a")) "," (Set (Var "b")))) & (Bool (Bool  "not" (Set (Var "a")) "," (Set (Var "p"))  ($#r1_parsp_1 :::"'||'"::: )  (Set (Var "a")) "," (Set (Var "c")))) & (Bool (Set (Var "a")) "," (Set (Var "p"))  ($#r1_parsp_1 :::"'||'"::: )  (Set (Var "b")) "," (Set (Var "q"))) & (Bool (Set (Var "a")) "," (Set (Var "p"))  ($#r1_parsp_1 :::"'||'"::: )  (Set (Var "c")) "," (Set (Var "r"))) & (Bool (Set (Var "a")) "," (Set (Var "b"))  ($#r1_parsp_1 :::"'||'"::: )  (Set (Var "p")) "," (Set (Var "q"))) & (Bool (Set (Var "a")) "," (Set (Var "c"))  ($#r1_parsp_1 :::"'||'"::: )  (Set (Var "p")) "," (Set (Var "r")))) "holds"  (Bool (Set (Var "b")) "," (Set (Var "c"))  ($#r1_parsp_1 :::"'||'"::: )  (Set (Var "q")) "," (Set (Var "r"))))) ; 
 definitionlet "IT" be   ($#l1_parsp_1 :::"ParSp":::); attr "IT" is  :::"FanodesSp-like":::  means :: PARSP_2:def 1 (Bool  "("  (Bool  "not" (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"   ($#m1_subset_1 :::"Element":::) "of" "IT" "holds"  (Bool (Set (Var "a")) "," (Set (Var "b"))  ($#r1_parsp_1 :::"'||'"::: )  (Set (Var "a")) "," (Set (Var "c"))))) & (Bool  "("   "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being"   ($#m1_subset_1 :::"Element":::) "of" "IT"  "st" (Bool (Bool (Set (Var "b")) "," (Set (Var "c"))  ($#r1_parsp_1 :::"'||'"::: )  (Set (Var "a")) "," (Set (Var "d"))) & (Bool (Set (Var "a")) "," (Set (Var "b"))  ($#r1_parsp_1 :::"'||'"::: )  (Set (Var "c")) "," (Set (Var "d"))) & (Bool (Set (Var "a")) "," (Set (Var "c"))  ($#r1_parsp_1 :::"'||'"::: )  (Set (Var "b")) "," (Set (Var "d")))) "holds"  (Bool (Set (Var "a")) "," (Set (Var "b"))  ($#r1_parsp_1 :::"'||'"::: )  (Set (Var "a")) "," (Set (Var "c")))  ")" ) & (Bool  "("   "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "being"   ($#m1_subset_1 :::"Element":::) "of" "IT"  "st" (Bool (Bool (Bool  "not" (Set (Var "a")) "," (Set (Var "p"))  ($#r1_parsp_1 :::"'||'"::: )  (Set (Var "a")) "," (Set (Var "b")))) & (Bool (Bool  "not" (Set (Var "a")) "," (Set (Var "p"))  ($#r1_parsp_1 :::"'||'"::: )  (Set (Var "a")) "," (Set (Var "c")))) & (Bool (Set (Var "a")) "," (Set (Var "p"))  ($#r1_parsp_1 :::"'||'"::: )  (Set (Var "b")) "," (Set (Var "q"))) & (Bool (Set (Var "a")) "," (Set (Var "p"))  ($#r1_parsp_1 :::"'||'"::: )  (Set (Var "c")) "," (Set (Var "r"))) & (Bool (Set (Var "a")) "," (Set (Var "b"))  ($#r1_parsp_1 :::"'||'"::: )  (Set (Var "p")) "," (Set (Var "q"))) & (Bool (Set (Var "a")) "," (Set (Var "c"))  ($#r1_parsp_1 :::"'||'"::: )  (Set (Var "p")) "," (Set (Var "r")))) "holds"  (Bool (Set (Var "b")) "," (Set (Var "c"))  ($#r1_parsp_1 :::"'||'"::: )  (Set (Var "q")) "," (Set (Var "r")))  ")" )  ")" ); end; 




:: deftheorem    defines :::"FanodesSp-like"::: PARSP_2:def 1 :  (Bool  "for" (Set (Var "IT")) "being"   ($#l1_parsp_1 :::"ParSp":::) "holds"   (Bool  "("  (Bool (Set (Var "IT")) "is"   ($#v1_parsp_2 :::"FanodesSp-like"::: )  ) "iff" (Bool  "("  (Bool  "not" (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT")) "holds"  (Bool (Set (Var "a")) "," (Set (Var "b"))  ($#r1_parsp_1 :::"'||'"::: )  (Set (Var "a")) "," (Set (Var "c"))))) & (Bool  "("   "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT"))  "st" (Bool (Bool (Set (Var "b")) "," (Set (Var "c"))  ($#r1_parsp_1 :::"'||'"::: )  (Set (Var "a")) "," (Set (Var "d"))) & (Bool (Set (Var "a")) "," (Set (Var "b"))  ($#r1_parsp_1 :::"'||'"::: )  (Set (Var "c")) "," (Set (Var "d"))) & (Bool (Set (Var "a")) "," (Set (Var "c"))  ($#r1_parsp_1 :::"'||'"::: )  (Set (Var "b")) "," (Set (Var "d")))) "holds"  (Bool (Set (Var "a")) "," (Set (Var "b"))  ($#r1_parsp_1 :::"'||'"::: )  (Set (Var "a")) "," (Set (Var "c")))  ")" ) & (Bool  "("   "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT"))  "st" (Bool (Bool (Bool  "not" (Set (Var "a")) "," (Set (Var "p"))  ($#r1_parsp_1 :::"'||'"::: )  (Set (Var "a")) "," (Set (Var "b")))) & (Bool (Bool  "not" (Set (Var "a")) "," (Set (Var "p"))  ($#r1_parsp_1 :::"'||'"::: )  (Set (Var "a")) "," (Set (Var "c")))) & (Bool (Set (Var "a")) "," (Set (Var "p"))  ($#r1_parsp_1 :::"'||'"::: )  (Set (Var "b")) "," (Set (Var "q"))) & (Bool (Set (Var "a")) "," (Set (Var "p"))  ($#r1_parsp_1 :::"'||'"::: )  (Set (Var "c")) "," (Set (Var "r"))) & (Bool (Set (Var "a")) "," (Set (Var "b"))  ($#r1_parsp_1 :::"'||'"::: )  (Set (Var "p")) "," (Set (Var "q"))) & (Bool (Set (Var "a")) "," (Set (Var "c"))  ($#r1_parsp_1 :::"'||'"::: )  (Set (Var "p")) "," (Set (Var "r")))) "holds"  (Bool (Set (Var "b")) "," (Set (Var "c"))  ($#r1_parsp_1 :::"'||'"::: )  (Set (Var "q")) "," (Set (Var "r")))  ")" )  ")" )  ")" )); 
 registration
cluster  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_parsp_1 :::"strict"::: )     ($#v2_parsp_1 :::"ParSp-like"::: )     ($#v1_parsp_2 :::"FanodesSp-like"::: )    for    ($#l1_parsp_1 :::"ParStr"::: )  ; 
end; definitionmode FanodesSp is   ($#v1_parsp_2 :::"FanodesSp-like"::: )    ($#l1_parsp_1 :::"ParSp":::); end; 
















theorem :: PARSP_2:9 (Bool  "for" (Set (Var "FdSp")) "being"   ($#l1_parsp_1 :::"FanodesSp":::)  (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "FdSp"))  "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 "FdSp")) "st" (Bool (Bool  "not" (Set (Var "p")) "," (Set (Var "q"))  ($#r1_parsp_1 :::"'||'"::: )  (Set (Var "p")) "," (Set (Var "r"))))))) ; 
 definitionlet "FdSp" be   ($#l1_parsp_1 :::"FanodesSp":::); let "a", "b", "c" be   ($#m1_subset_1 :::"Element":::) "of" (Set (Const "FdSp")); pred "a" "," "b" "," "c" :::"is_collinear":::  means :: PARSP_2:def 2 (Bool "a" "," "b"  ($#r1_parsp_1 :::"'||'"::: )  "a" "," "c"); end; 







:: deftheorem    defines :::"is_collinear"::: PARSP_2:def 2 :  (Bool  "for" (Set (Var "FdSp")) "being"   ($#l1_parsp_1 :::"FanodesSp":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "FdSp")) "holds"   (Bool  "("  (Bool (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c"))  ($#r1_parsp_2 :::"is_collinear"::: )  ) "iff" (Bool (Set (Var "a")) "," (Set (Var "b"))  ($#r1_parsp_1 :::"'||'"::: )  (Set (Var "a")) "," (Set (Var "c")))  ")" ))); 
 
theorem :: PARSP_2:10 (Bool  "for" (Set (Var "FdSp")) "being"   ($#l1_parsp_1 :::"FanodesSp":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "FdSp"))  "st" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c"))  ($#r1_parsp_2 :::"is_collinear"::: )  )) "holds"  (Bool  "("  (Bool (Set (Var "a")) "," (Set (Var "c")) "," (Set (Var "b"))  ($#r1_parsp_2 :::"is_collinear"::: )  ) & (Bool (Set (Var "c")) "," (Set (Var "b")) "," (Set (Var "a"))  ($#r1_parsp_2 :::"is_collinear"::: )  ) & (Bool (Set (Var "b")) "," (Set (Var "a")) "," (Set (Var "c"))  ($#r1_parsp_2 :::"is_collinear"::: )  ) & (Bool (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "a"))  ($#r1_parsp_2 :::"is_collinear"::: )  ) & (Bool (Set (Var "c")) "," (Set (Var "a")) "," (Set (Var "b"))  ($#r1_parsp_2 :::"is_collinear"::: )  )  ")" ))) ; 
 
theorem :: PARSP_2:11 (Bool  "for" (Set (Var "FdSp")) "being"   ($#l1_parsp_1 :::"FanodesSp":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "FdSp"))  "st" (Bool (Bool (Bool  "not" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c"))  ($#r1_parsp_2 :::"is_collinear"::: )  )) & (Bool (Set (Var "a")) "," (Set (Var "b"))  ($#r1_parsp_1 :::"'||'"::: )  (Set (Var "p")) "," (Set (Var "q"))) & (Bool (Set (Var "a")) "," (Set (Var "c"))  ($#r1_parsp_1 :::"'||'"::: )  (Set (Var "p")) "," (Set (Var "r"))) & (Bool (Set (Var "p"))  ($#r1_hidden :::"<>"::: )  (Set (Var "q"))) & (Bool (Set (Var "p"))  ($#r1_hidden :::"<>"::: )  (Set (Var "r")))) "holds"  (Bool  "not" (Bool (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r"))  ($#r1_parsp_2 :::"is_collinear"::: )  )))) ; 
 
theorem :: PARSP_2:12 (Bool  "for" (Set (Var "FdSp")) "being"   ($#l1_parsp_1 :::"FanodesSp":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "FdSp"))  "st" (Bool (Bool  "("  (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set (Var "b"))) "or" (Bool (Set (Var "b"))  ($#r1_hidden :::"="::: )  (Set (Var "c"))) "or" (Bool (Set (Var "c"))  ($#r1_hidden :::"="::: )  (Set (Var "a")))  ")" )) "holds"  (Bool (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c"))  ($#r1_parsp_2 :::"is_collinear"::: )  ))) ; 
 
theorem :: PARSP_2:13 (Bool  "for" (Set (Var "FdSp")) "being"   ($#l1_parsp_1 :::"FanodesSp":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "FdSp"))  "st" (Bool (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set (Var "b"))) & (Bool (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "p"))  ($#r1_parsp_2 :::"is_collinear"::: )  ) & (Bool (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "q"))  ($#r1_parsp_2 :::"is_collinear"::: )  ) & (Bool (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "r"))  ($#r1_parsp_2 :::"is_collinear"::: )  )) "holds"  (Bool (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r"))  ($#r1_parsp_2 :::"is_collinear"::: )  ))) ; 
 
theorem :: PARSP_2:14 (Bool  "for" (Set (Var "FdSp")) "being"   ($#l1_parsp_1 :::"FanodesSp":::)  (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "FdSp"))  "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 "FdSp")) "st" (Bool (Bool  "not" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r"))  ($#r1_parsp_2 :::"is_collinear"::: )  ))))) ; 
 
theorem :: PARSP_2:15 (Bool  "for" (Set (Var "FdSp")) "being"   ($#l1_parsp_1 :::"FanodesSp":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "FdSp"))  "st" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c"))  ($#r1_parsp_2 :::"is_collinear"::: )  ) & (Bool (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "d"))  ($#r1_parsp_2 :::"is_collinear"::: )  )) "holds"  (Bool (Set (Var "a")) "," (Set (Var "b"))  ($#r1_parsp_1 :::"'||'"::: )  (Set (Var "c")) "," (Set (Var "d"))))) ; 
 
theorem :: PARSP_2:16 (Bool  "for" (Set (Var "FdSp")) "being"   ($#l1_parsp_1 :::"FanodesSp":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "FdSp"))  "st" (Bool (Bool (Bool  "not" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c"))  ($#r1_parsp_2 :::"is_collinear"::: )  )) & (Bool (Set (Var "a")) "," (Set (Var "b"))  ($#r1_parsp_1 :::"'||'"::: )  (Set (Var "c")) "," (Set (Var "d")))) "holds"  (Bool  "not" (Bool (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "d"))  ($#r1_parsp_2 :::"is_collinear"::: )  )))) ; 
 
theorem :: PARSP_2:17 (Bool  "for" (Set (Var "FdSp")) "being"   ($#l1_parsp_1 :::"FanodesSp":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "FdSp"))  "st" (Bool (Bool (Bool  "not" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c"))  ($#r1_parsp_2 :::"is_collinear"::: )  )) & (Bool (Set (Var "a")) "," (Set (Var "b"))  ($#r1_parsp_1 :::"'||'"::: )  (Set (Var "c")) "," (Set (Var "d"))) & (Bool (Set (Var "c"))  ($#r1_hidden :::"<>"::: )  (Set (Var "d"))) & (Bool (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "x"))  ($#r1_parsp_2 :::"is_collinear"::: )  )) "holds"  (Bool  "not" (Bool (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "x"))  ($#r1_parsp_2 :::"is_collinear"::: )  )))) ; 
 
theorem :: PARSP_2:18 (Bool  "for" (Set (Var "FdSp")) "being"   ($#l1_parsp_1 :::"FanodesSp":::)  (Bool  "for" (Set (Var "o")) "," (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "FdSp"))  "holds"  (Bool  "("  (Bool (Set (Var "o")) "," (Set (Var "a")) "," (Set (Var "b"))  ($#r1_parsp_2 :::"is_collinear"::: )  ) "or"  "not" (Bool (Set (Var "o")) "," (Set (Var "a")) "," (Set (Var "x"))  ($#r1_parsp_2 :::"is_collinear"::: )  ) "or"  "not" (Bool (Set (Var "o")) "," (Set (Var "b")) "," (Set (Var "x"))  ($#r1_parsp_2 :::"is_collinear"::: )  ) "or" (Bool (Set (Var "o"))  ($#r1_hidden :::"="::: )  (Set (Var "x")))  ")" ))) ; 
 
theorem :: PARSP_2:19 (Bool  "for" (Set (Var "FdSp")) "being"   ($#l1_parsp_1 :::"FanodesSp":::)  (Bool  "for" (Set (Var "o")) "," (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "p")) "," (Set (Var "q")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "FdSp"))  "st" (Bool (Bool (Set (Var "o"))  ($#r1_hidden :::"<>"::: )  (Set (Var "a"))) & (Bool (Set (Var "o"))  ($#r1_hidden :::"<>"::: )  (Set (Var "b"))) & (Bool (Set (Var "o")) "," (Set (Var "a")) "," (Set (Var "b"))  ($#r1_parsp_2 :::"is_collinear"::: )  ) & (Bool (Set (Var "o")) "," (Set (Var "a")) "," (Set (Var "p"))  ($#r1_parsp_2 :::"is_collinear"::: )  ) & (Bool (Set (Var "o")) "," (Set (Var "b")) "," (Set (Var "q"))  ($#r1_parsp_2 :::"is_collinear"::: )  )) "holds"  (Bool (Set (Var "a")) "," (Set (Var "b"))  ($#r1_parsp_1 :::"'||'"::: )  (Set (Var "p")) "," (Set (Var "q"))))) ; 
 
theorem :: PARSP_2:20 (Bool  "for" (Set (Var "FdSp")) "being"   ($#l1_parsp_1 :::"FanodesSp":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "p")) "," (Set (Var "q")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "FdSp"))  "st" (Bool (Bool (Bool  "not" (Set (Var "a")) "," (Set (Var "b"))  ($#r1_parsp_1 :::"'||'"::: )  (Set (Var "c")) "," (Set (Var "d")))) & (Bool (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "p"))  ($#r1_parsp_2 :::"is_collinear"::: )  ) & (Bool (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "q"))  ($#r1_parsp_2 :::"is_collinear"::: )  ) & (Bool (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "p"))  ($#r1_parsp_2 :::"is_collinear"::: )  ) & (Bool (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "q"))  ($#r1_parsp_2 :::"is_collinear"::: )  )) "holds"  (Bool (Set (Var "p"))  ($#r1_hidden :::"="::: )  (Set (Var "q"))))) ; 
 
theorem :: PARSP_2:21 (Bool  "for" (Set (Var "FdSp")) "being"   ($#l1_parsp_1 :::"FanodesSp":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "FdSp"))  "st" (Bool (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set (Var "b"))) & (Bool (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c"))  ($#r1_parsp_2 :::"is_collinear"::: )  ) & (Bool (Set (Var "a")) "," (Set (Var "b"))  ($#r1_parsp_1 :::"'||'"::: )  (Set (Var "c")) "," (Set (Var "d")))) "holds"  (Bool (Set (Var "a")) "," (Set (Var "c"))  ($#r1_parsp_1 :::"'||'"::: )  (Set (Var "b")) "," (Set (Var "d"))))) ; 
 
theorem :: PARSP_2:22 (Bool  "for" (Set (Var "FdSp")) "being"   ($#l1_parsp_1 :::"FanodesSp":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "FdSp"))  "st" (Bool (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set (Var "b"))) & (Bool (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c"))  ($#r1_parsp_2 :::"is_collinear"::: )  ) & (Bool (Set (Var "a")) "," (Set (Var "b"))  ($#r1_parsp_1 :::"'||'"::: )  (Set (Var "c")) "," (Set (Var "d")))) "holds"  (Bool (Set (Var "c")) "," (Set (Var "b"))  ($#r1_parsp_1 :::"'||'"::: )  (Set (Var "c")) "," (Set (Var "d"))))) ; 
 
theorem :: PARSP_2:23 (Bool  "for" (Set (Var "FdSp")) "being"   ($#l1_parsp_1 :::"FanodesSp":::)  (Bool  "for" (Set (Var "o")) "," (Set (Var "a")) "," (Set (Var "c")) "," (Set (Var "b")) "," (Set (Var "p")) "," (Set (Var "q")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "FdSp"))  "st" (Bool (Bool (Bool  "not" (Set (Var "o")) "," (Set (Var "a")) "," (Set (Var "c"))  ($#r1_parsp_2 :::"is_collinear"::: )  )) & (Bool (Set (Var "o")) "," (Set (Var "a")) "," (Set (Var "b"))  ($#r1_parsp_2 :::"is_collinear"::: )  ) & (Bool (Set (Var "o")) "," (Set (Var "c")) "," (Set (Var "p"))  ($#r1_parsp_2 :::"is_collinear"::: )  ) & (Bool (Set (Var "o")) "," (Set (Var "c")) "," (Set (Var "q"))  ($#r1_parsp_2 :::"is_collinear"::: )  ) & (Bool (Set (Var "a")) "," (Set (Var "c"))  ($#r1_parsp_1 :::"'||'"::: )  (Set (Var "b")) "," (Set (Var "p"))) & (Bool (Set (Var "a")) "," (Set (Var "c"))  ($#r1_parsp_1 :::"'||'"::: )  (Set (Var "b")) "," (Set (Var "q")))) "holds"  (Bool (Set (Var "p"))  ($#r1_hidden :::"="::: )  (Set (Var "q"))))) ; 
 
theorem :: PARSP_2:24 (Bool  "for" (Set (Var "FdSp")) "being"   ($#l1_parsp_1 :::"FanodesSp":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "FdSp"))  "st" (Bool (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set (Var "b"))) & (Bool (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c"))  ($#r1_parsp_2 :::"is_collinear"::: )  ) & (Bool (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "d"))  ($#r1_parsp_2 :::"is_collinear"::: )  )) "holds"  (Bool (Set (Var "a")) "," (Set (Var "c")) "," (Set (Var "d"))  ($#r1_parsp_2 :::"is_collinear"::: )  ))) ; 
 
theorem :: PARSP_2:25 (Bool  "for" (Set (Var "FdSp")) "being"   ($#l1_parsp_1 :::"FanodesSp":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "FdSp"))  "st" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c"))  ($#r1_parsp_2 :::"is_collinear"::: )  ) & (Bool (Set (Var "a")) "," (Set (Var "c")) "," (Set (Var "d"))  ($#r1_parsp_2 :::"is_collinear"::: )  ) & (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set (Var "c")))) "holds"  (Bool (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d"))  ($#r1_parsp_2 :::"is_collinear"::: )  ))) ; 
 definitionlet "FdSp" be   ($#l1_parsp_1 :::"FanodesSp":::); let "a", "b", "c", "d" be   ($#m1_subset_1 :::"Element":::) "of" (Set (Const "FdSp")); pred  :::"parallelogram"::: "a" "," "b" "," "c" "," "d" means :: PARSP_2:def 3 (Bool  "("  (Bool (Bool  "not" "a" "," "b" "," "c"  ($#r1_parsp_2 :::"is_collinear"::: )  )) & (Bool "a" "," "b"  ($#r1_parsp_1 :::"'||'"::: )  "c" "," "d") & (Bool "a" "," "c"  ($#r1_parsp_1 :::"'||'"::: )  "b" "," "d")  ")" ); end; 








:: deftheorem    defines :::"parallelogram"::: PARSP_2:def 3 :  (Bool  "for" (Set (Var "FdSp")) "being"   ($#l1_parsp_1 :::"FanodesSp":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "FdSp")) "holds"   (Bool  "("  (Bool   ($#r2_parsp_2 :::"parallelogram"::: )  (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d"))) "iff" (Bool  "("  (Bool (Bool  "not" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c"))  ($#r1_parsp_2 :::"is_collinear"::: )  )) & (Bool (Set (Var "a")) "," (Set (Var "b"))  ($#r1_parsp_1 :::"'||'"::: )  (Set (Var "c")) "," (Set (Var "d"))) & (Bool (Set (Var "a")) "," (Set (Var "c"))  ($#r1_parsp_1 :::"'||'"::: )  (Set (Var "b")) "," (Set (Var "d")))  ")" )  ")" ))); 
 
theorem :: PARSP_2:26 (Bool  "for" (Set (Var "FdSp")) "being"   ($#l1_parsp_1 :::"FanodesSp":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "FdSp"))  "st" (Bool (Bool   ($#r2_parsp_2 :::"parallelogram"::: )  (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")))) "holds"  (Bool  "("  (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set (Var "b"))) & (Bool (Set (Var "b"))  ($#r1_hidden :::"<>"::: )  (Set (Var "c"))) & (Bool (Set (Var "c"))  ($#r1_hidden :::"<>"::: )  (Set (Var "a"))) & (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set (Var "d"))) & (Bool (Set (Var "b"))  ($#r1_hidden :::"<>"::: )  (Set (Var "d"))) & (Bool (Set (Var "c"))  ($#r1_hidden :::"<>"::: )  (Set (Var "d")))  ")" ))) ; 
 
theorem :: PARSP_2:27 (Bool  "for" (Set (Var "FdSp")) "being"   ($#l1_parsp_1 :::"FanodesSp":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "FdSp"))  "st" (Bool (Bool   ($#r2_parsp_2 :::"parallelogram"::: )  (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")))) "holds"  (Bool  "("  (Bool (Bool  "not" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c"))  ($#r1_parsp_2 :::"is_collinear"::: )  )) & (Bool (Bool  "not" (Set (Var "b")) "," (Set (Var "a")) "," (Set (Var "d"))  ($#r1_parsp_2 :::"is_collinear"::: )  )) & (Bool (Bool  "not" (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "a"))  ($#r1_parsp_2 :::"is_collinear"::: )  )) & (Bool (Bool  "not" (Set (Var "d")) "," (Set (Var "c")) "," (Set (Var "b"))  ($#r1_parsp_2 :::"is_collinear"::: )  ))  ")" ))) ; 
 
theorem :: PARSP_2:28 (Bool  "for" (Set (Var "FdSp")) "being"   ($#l1_parsp_1 :::"FanodesSp":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "FdSp"))  "st" (Bool (Bool   ($#r2_parsp_2 :::"parallelogram"::: )  (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")))) "holds"  (Bool  "("  (Bool (Bool  "not" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c"))  ($#r1_parsp_2 :::"is_collinear"::: )  )) & (Bool (Bool  "not" (Set (Var "b")) "," (Set (Var "a")) "," (Set (Var "d"))  ($#r1_parsp_2 :::"is_collinear"::: )  )) & (Bool (Bool  "not" (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "a"))  ($#r1_parsp_2 :::"is_collinear"::: )  )) & (Bool (Bool  "not" (Set (Var "d")) "," (Set (Var "c")) "," (Set (Var "b"))  ($#r1_parsp_2 :::"is_collinear"::: )  )) & (Bool (Bool  "not" (Set (Var "a")) "," (Set (Var "c")) "," (Set (Var "b"))  ($#r1_parsp_2 :::"is_collinear"::: )  )) & (Bool (Bool  "not" (Set (Var "b")) "," (Set (Var "a")) "," (Set (Var "c"))  ($#r1_parsp_2 :::"is_collinear"::: )  )) & (Bool (Bool  "not" (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "a"))  ($#r1_parsp_2 :::"is_collinear"::: )  )) & (Bool (Bool  "not" (Set (Var "c")) "," (Set (Var "a")) "," (Set (Var "b"))  ($#r1_parsp_2 :::"is_collinear"::: )  )) & (Bool (Bool  "not" (Set (Var "c")) "," (Set (Var "b")) "," (Set (Var "a"))  ($#r1_parsp_2 :::"is_collinear"::: )  )) & (Bool (Bool  "not" (Set (Var "b")) "," (Set (Var "d")) "," (Set (Var "a"))  ($#r1_parsp_2 :::"is_collinear"::: )  )) & (Bool (Bool  "not" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "d"))  ($#r1_parsp_2 :::"is_collinear"::: )  )) & (Bool (Bool  "not" (Set (Var "a")) "," (Set (Var "d")) "," (Set (Var "b"))  ($#r1_parsp_2 :::"is_collinear"::: )  )) & (Bool (Bool  "not" (Set (Var "d")) "," (Set (Var "a")) "," (Set (Var "b"))  ($#r1_parsp_2 :::"is_collinear"::: )  )) & (Bool (Bool  "not" (Set (Var "d")) "," (Set (Var "b")) "," (Set (Var "a"))  ($#r1_parsp_2 :::"is_collinear"::: )  )) & (Bool (Bool  "not" (Set (Var "c")) "," (Set (Var "a")) "," (Set (Var "d"))  ($#r1_parsp_2 :::"is_collinear"::: )  )) & (Bool (Bool  "not" (Set (Var "a")) "," (Set (Var "c")) "," (Set (Var "d"))  ($#r1_parsp_2 :::"is_collinear"::: )  )) & (Bool (Bool  "not" (Set (Var "a")) "," (Set (Var "d")) "," (Set (Var "c"))  ($#r1_parsp_2 :::"is_collinear"::: )  )) & (Bool (Bool  "not" (Set (Var "d")) "," (Set (Var "a")) "," (Set (Var "c"))  ($#r1_parsp_2 :::"is_collinear"::: )  )) & (Bool (Bool  "not" (Set (Var "d")) "," (Set (Var "c")) "," (Set (Var "a"))  ($#r1_parsp_2 :::"is_collinear"::: )  )) & (Bool (Bool  "not" (Set (Var "d")) "," (Set (Var "b")) "," (Set (Var "c"))  ($#r1_parsp_2 :::"is_collinear"::: )  )) & (Bool (Bool  "not" (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d"))  ($#r1_parsp_2 :::"is_collinear"::: )  )) & (Bool (Bool  "not" (Set (Var "b")) "," (Set (Var "d")) "," (Set (Var "c"))  ($#r1_parsp_2 :::"is_collinear"::: )  )) & (Bool (Bool  "not" (Set (Var "c")) "," (Set (Var "b")) "," (Set (Var "d"))  ($#r1_parsp_2 :::"is_collinear"::: )  )) & (Bool (Bool  "not" (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "b"))  ($#r1_parsp_2 :::"is_collinear"::: )  ))  ")" ))) ; 
 
theorem :: PARSP_2:29 (Bool  "for" (Set (Var "FdSp")) "being"   ($#l1_parsp_1 :::"FanodesSp":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "FdSp"))  "holds"  (Bool  "("   "not" (Bool   ($#r2_parsp_2 :::"parallelogram"::: )  (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d"))) "or"  "not" (Bool (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "x"))  ($#r1_parsp_2 :::"is_collinear"::: )  ) "or"  "not" (Bool (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "x"))  ($#r1_parsp_2 :::"is_collinear"::: )  )  ")" ))) ; 
 
theorem :: PARSP_2:30 (Bool  "for" (Set (Var "FdSp")) "being"   ($#l1_parsp_1 :::"FanodesSp":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "FdSp"))  "st" (Bool (Bool   ($#r2_parsp_2 :::"parallelogram"::: )  (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")))) "holds"  (Bool   ($#r2_parsp_2 :::"parallelogram"::: )  (Set (Var "a")) "," (Set (Var "c")) "," (Set (Var "b")) "," (Set (Var "d"))))) ; 
 
theorem :: PARSP_2:31 (Bool  "for" (Set (Var "FdSp")) "being"   ($#l1_parsp_1 :::"FanodesSp":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "FdSp"))  "st" (Bool (Bool   ($#r2_parsp_2 :::"parallelogram"::: )  (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")))) "holds"  (Bool   ($#r2_parsp_2 :::"parallelogram"::: )  (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "a")) "," (Set (Var "b"))))) ; 
 
theorem :: PARSP_2:32 (Bool  "for" (Set (Var "FdSp")) "being"   ($#l1_parsp_1 :::"FanodesSp":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "FdSp"))  "st" (Bool (Bool   ($#r2_parsp_2 :::"parallelogram"::: )  (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")))) "holds"  (Bool   ($#r2_parsp_2 :::"parallelogram"::: )  (Set (Var "b")) "," (Set (Var "a")) "," (Set (Var "d")) "," (Set (Var "c"))))) ; 
 
theorem :: PARSP_2:33 (Bool  "for" (Set (Var "FdSp")) "being"   ($#l1_parsp_1 :::"FanodesSp":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "FdSp"))  "st" (Bool (Bool   ($#r2_parsp_2 :::"parallelogram"::: )  (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")))) "holds"  (Bool  "("  (Bool   ($#r2_parsp_2 :::"parallelogram"::: )  (Set (Var "a")) "," (Set (Var "c")) "," (Set (Var "b")) "," (Set (Var "d"))) & (Bool   ($#r2_parsp_2 :::"parallelogram"::: )  (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "a")) "," (Set (Var "b"))) & (Bool   ($#r2_parsp_2 :::"parallelogram"::: )  (Set (Var "b")) "," (Set (Var "a")) "," (Set (Var "d")) "," (Set (Var "c"))) & (Bool   ($#r2_parsp_2 :::"parallelogram"::: )  (Set (Var "c")) "," (Set (Var "a")) "," (Set (Var "d")) "," (Set (Var "b"))) & (Bool   ($#r2_parsp_2 :::"parallelogram"::: )  (Set (Var "d")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "a"))) & (Bool   ($#r2_parsp_2 :::"parallelogram"::: )  (Set (Var "b")) "," (Set (Var "d")) "," (Set (Var "a")) "," (Set (Var "c"))) & (Bool   ($#r2_parsp_2 :::"parallelogram"::: )  (Set (Var "d")) "," (Set (Var "c")) "," (Set (Var "b")) "," (Set (Var "a")))  ")" ))) ; 
 
theorem :: PARSP_2:34 (Bool  "for" (Set (Var "FdSp")) "being"   ($#l1_parsp_1 :::"FanodesSp":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "FdSp"))  "st" (Bool (Bool (Bool  "not" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c"))  ($#r1_parsp_2 :::"is_collinear"::: )  ))) "holds"  (Bool  "ex" (Set (Var "d")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "FdSp")) "st" (Bool   ($#r2_parsp_2 :::"parallelogram"::: )  (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")))))) ; 
 
theorem :: PARSP_2:35 (Bool  "for" (Set (Var "FdSp")) "being"   ($#l1_parsp_1 :::"FanodesSp":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "p")) "," (Set (Var "q")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "FdSp"))  "st" (Bool (Bool   ($#r2_parsp_2 :::"parallelogram"::: )  (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "p"))) & (Bool   ($#r2_parsp_2 :::"parallelogram"::: )  (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "q")))) "holds"  (Bool (Set (Var "p"))  ($#r1_hidden :::"="::: )  (Set (Var "q"))))) ; 
 
theorem :: PARSP_2:36 (Bool  "for" (Set (Var "FdSp")) "being"   ($#l1_parsp_1 :::"FanodesSp":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "FdSp"))  "st" (Bool (Bool   ($#r2_parsp_2 :::"parallelogram"::: )  (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")))) "holds"  (Bool  "not" (Bool (Set (Var "a")) "," (Set (Var "d"))  ($#r1_parsp_1 :::"'||'"::: )  (Set (Var "b")) "," (Set (Var "c")))))) ; 
 
theorem :: PARSP_2:37 (Bool  "for" (Set (Var "FdSp")) "being"   ($#l1_parsp_1 :::"FanodesSp":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "FdSp"))  "st" (Bool (Bool   ($#r2_parsp_2 :::"parallelogram"::: )  (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")))) "holds"  (Bool  "not" (Bool   ($#r2_parsp_2 :::"parallelogram"::: )  (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "d")) "," (Set (Var "c")))))) ; 
 
theorem :: PARSP_2:38 (Bool  "for" (Set (Var "FdSp")) "being"   ($#l1_parsp_1 :::"FanodesSp":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "FdSp"))  "st" (Bool (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set (Var "b")))) "holds"  (Bool  "ex" (Set (Var "c")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "FdSp")) "st"  (Bool  "("  (Bool (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c"))  ($#r1_parsp_2 :::"is_collinear"::: )  ) & (Bool (Set (Var "c"))  ($#r1_hidden :::"<>"::: )  (Set (Var "a"))) & (Bool (Set (Var "c"))  ($#r1_hidden :::"<>"::: )  (Set (Var "b")))  ")" )))) ; 
 
theorem :: PARSP_2:39 (Bool  "for" (Set (Var "FdSp")) "being"   ($#l1_parsp_1 :::"FanodesSp":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "p")) "," (Set (Var "b")) "," (Set (Var "q")) "," (Set (Var "c")) "," (Set (Var "r")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "FdSp"))  "st" (Bool (Bool   ($#r2_parsp_2 :::"parallelogram"::: )  (Set (Var "a")) "," (Set (Var "p")) "," (Set (Var "b")) "," (Set (Var "q"))) & (Bool   ($#r2_parsp_2 :::"parallelogram"::: )  (Set (Var "a")) "," (Set (Var "p")) "," (Set (Var "c")) "," (Set (Var "r")))) "holds"  (Bool (Set (Var "b")) "," (Set (Var "c"))  ($#r1_parsp_1 :::"'||'"::: )  (Set (Var "q")) "," (Set (Var "r"))))) ; 
 
theorem :: PARSP_2:40 (Bool  "for" (Set (Var "FdSp")) "being"   ($#l1_parsp_1 :::"FanodesSp":::)  (Bool  "for" (Set (Var "b")) "," (Set (Var "q")) "," (Set (Var "c")) "," (Set (Var "a")) "," (Set (Var "p")) "," (Set (Var "r")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "FdSp"))  "st" (Bool (Bool (Bool  "not" (Set (Var "b")) "," (Set (Var "q")) "," (Set (Var "c"))  ($#r1_parsp_2 :::"is_collinear"::: )  )) & (Bool   ($#r2_parsp_2 :::"parallelogram"::: )  (Set (Var "a")) "," (Set (Var "p")) "," (Set (Var "b")) "," (Set (Var "q"))) & (Bool   ($#r2_parsp_2 :::"parallelogram"::: )  (Set (Var "a")) "," (Set (Var "p")) "," (Set (Var "c")) "," (Set (Var "r")))) "holds"  (Bool   ($#r2_parsp_2 :::"parallelogram"::: )  (Set (Var "b")) "," (Set (Var "q")) "," (Set (Var "c")) "," (Set (Var "r"))))) ; 
 
theorem :: PARSP_2:41 (Bool  "for" (Set (Var "FdSp")) "being"   ($#l1_parsp_1 :::"FanodesSp":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "FdSp"))  "st" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c"))  ($#r1_parsp_2 :::"is_collinear"::: )  ) & (Bool (Set (Var "b"))  ($#r1_hidden :::"<>"::: )  (Set (Var "c"))) & (Bool   ($#r2_parsp_2 :::"parallelogram"::: )  (Set (Var "a")) "," (Set (Var "p")) "," (Set (Var "b")) "," (Set (Var "q"))) & (Bool   ($#r2_parsp_2 :::"parallelogram"::: )  (Set (Var "a")) "," (Set (Var "p")) "," (Set (Var "c")) "," (Set (Var "r")))) "holds"  (Bool   ($#r2_parsp_2 :::"parallelogram"::: )  (Set (Var "b")) "," (Set (Var "q")) "," (Set (Var "c")) "," (Set (Var "r"))))) ; 
 
theorem :: PARSP_2:42 (Bool  "for" (Set (Var "FdSp")) "being"   ($#l1_parsp_1 :::"FanodesSp":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "p")) "," (Set (Var "b")) "," (Set (Var "q")) "," (Set (Var "c")) "," (Set (Var "r")) "," (Set (Var "d")) "," (Set (Var "s")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "FdSp"))  "st" (Bool (Bool   ($#r2_parsp_2 :::"parallelogram"::: )  (Set (Var "a")) "," (Set (Var "p")) "," (Set (Var "b")) "," (Set (Var "q"))) & (Bool   ($#r2_parsp_2 :::"parallelogram"::: )  (Set (Var "a")) "," (Set (Var "p")) "," (Set (Var "c")) "," (Set (Var "r"))) & (Bool   ($#r2_parsp_2 :::"parallelogram"::: )  (Set (Var "b")) "," (Set (Var "q")) "," (Set (Var "d")) "," (Set (Var "s")))) "holds"  (Bool (Set (Var "c")) "," (Set (Var "d"))  ($#r1_parsp_1 :::"'||'"::: )  (Set (Var "r")) "," (Set (Var "s"))))) ; 
 
theorem :: PARSP_2:43 (Bool  "for" (Set (Var "FdSp")) "being"   ($#l1_parsp_1 :::"FanodesSp":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "FdSp"))  "st" (Bool (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set (Var "b")))) "holds"  (Bool  "ex" (Set (Var "c")) "," (Set (Var "d")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "FdSp")) "st" (Bool   ($#r2_parsp_2 :::"parallelogram"::: )  (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")))))) ; 
 
theorem :: PARSP_2:44 (Bool  "for" (Set (Var "FdSp")) "being"   ($#l1_parsp_1 :::"FanodesSp":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "d")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "FdSp"))  "st" (Bool (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set (Var "d")))) "holds"  (Bool  "ex" (Set (Var "b")) "," (Set (Var "c")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "FdSp")) "st" (Bool   ($#r2_parsp_2 :::"parallelogram"::: )  (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")))))) ; 
 definitionlet "FdSp" be   ($#l1_parsp_1 :::"FanodesSp":::); let "a", "b", "r", "s" be   ($#m1_subset_1 :::"Element":::) "of" (Set (Const "FdSp")); pred "a" "," "b" :::"congr"::: "r" "," "s" means :: PARSP_2:def 4 (Bool  "("  (Bool  "("  (Bool "a"  ($#r1_hidden :::"="::: )  "b") & (Bool "r"  ($#r1_hidden :::"="::: )  "s")  ")" ) "or" (Bool  "ex" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#m1_subset_1 :::"Element":::) "of" "FdSp" "st"  (Bool  "("  (Bool   ($#r2_parsp_2 :::"parallelogram"::: )  (Set (Var "p")) "," (Set (Var "q")) "," "a" "," "b") & (Bool   ($#r2_parsp_2 :::"parallelogram"::: )  (Set (Var "p")) "," (Set (Var "q")) "," "r" "," "s")  ")" ))  ")" ); end; 








:: deftheorem    defines :::"congr"::: PARSP_2:def 4 :  (Bool  "for" (Set (Var "FdSp")) "being"   ($#l1_parsp_1 :::"FanodesSp":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "r")) "," (Set (Var "s")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "FdSp")) "holds"   (Bool  "("  (Bool (Set (Var "a")) "," (Set (Var "b"))  ($#r3_parsp_2 :::"congr"::: )  (Set (Var "r")) "," (Set (Var "s"))) "iff" (Bool  "("  (Bool  "("  (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set (Var "b"))) & (Bool (Set (Var "r"))  ($#r1_hidden :::"="::: )  (Set (Var "s")))  ")" ) "or" (Bool  "ex" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "FdSp")) "st"  (Bool  "("  (Bool   ($#r2_parsp_2 :::"parallelogram"::: )  (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "a")) "," (Set (Var "b"))) & (Bool   ($#r2_parsp_2 :::"parallelogram"::: )  (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "," (Set (Var "s")))  ")" ))  ")" )  ")" ))); 
 
theorem :: PARSP_2:45 (Bool  "for" (Set (Var "FdSp")) "being"   ($#l1_parsp_1 :::"FanodesSp":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "FdSp"))  "st" (Bool (Bool (Set (Var "a")) "," (Set (Var "a"))  ($#r3_parsp_2 :::"congr"::: )  (Set (Var "b")) "," (Set (Var "c")))) "holds"  (Bool (Set (Var "b"))  ($#r1_hidden :::"="::: )  (Set (Var "c"))))) ; 
 
theorem :: PARSP_2:46 (Bool  "for" (Set (Var "FdSp")) "being"   ($#l1_parsp_1 :::"FanodesSp":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "FdSp"))  "st" (Bool (Bool (Set (Var "a")) "," (Set (Var "b"))  ($#r3_parsp_2 :::"congr"::: )  (Set (Var "c")) "," (Set (Var "c")))) "holds"  (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set (Var "b"))))) ; 
 
theorem :: PARSP_2:47 (Bool  "for" (Set (Var "FdSp")) "being"   ($#l1_parsp_1 :::"FanodesSp":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "FdSp"))  "st" (Bool (Bool (Set (Var "a")) "," (Set (Var "b"))  ($#r3_parsp_2 :::"congr"::: )  (Set (Var "b")) "," (Set (Var "a")))) "holds"  (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set (Var "b"))))) ; 
 
theorem :: PARSP_2:48 (Bool  "for" (Set (Var "FdSp")) "being"   ($#l1_parsp_1 :::"FanodesSp":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "FdSp"))  "st" (Bool (Bool (Set (Var "a")) "," (Set (Var "b"))  ($#r3_parsp_2 :::"congr"::: )  (Set (Var "c")) "," (Set (Var "d")))) "holds"  (Bool (Set (Var "a")) "," (Set (Var "b"))  ($#r1_parsp_1 :::"'||'"::: )  (Set (Var "c")) "," (Set (Var "d"))))) ; 
 
theorem :: PARSP_2:49 (Bool  "for" (Set (Var "FdSp")) "being"   ($#l1_parsp_1 :::"FanodesSp":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "FdSp"))  "st" (Bool (Bool (Set (Var "a")) "," (Set (Var "b"))  ($#r3_parsp_2 :::"congr"::: )  (Set (Var "c")) "," (Set (Var "d")))) "holds"  (Bool (Set (Var "a")) "," (Set (Var "c"))  ($#r1_parsp_1 :::"'||'"::: )  (Set (Var "b")) "," (Set (Var "d"))))) ; 
 
theorem :: PARSP_2:50 (Bool  "for" (Set (Var "FdSp")) "being"   ($#l1_parsp_1 :::"FanodesSp":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "FdSp"))  "st" (Bool (Bool (Set (Var "a")) "," (Set (Var "b"))  ($#r3_parsp_2 :::"congr"::: )  (Set (Var "c")) "," (Set (Var "d"))) & (Bool (Bool  "not" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c"))  ($#r1_parsp_2 :::"is_collinear"::: )  ))) "holds"  (Bool   ($#r2_parsp_2 :::"parallelogram"::: )  (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d"))))) ; 
 
theorem :: PARSP_2:51 (Bool  "for" (Set (Var "FdSp")) "being"   ($#l1_parsp_1 :::"FanodesSp":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "FdSp"))  "st" (Bool (Bool   ($#r2_parsp_2 :::"parallelogram"::: )  (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")))) "holds"  (Bool (Set (Var "a")) "," (Set (Var "b"))  ($#r3_parsp_2 :::"congr"::: )  (Set (Var "c")) "," (Set (Var "d"))))) ; 
 
theorem :: PARSP_2:52 (Bool  "for" (Set (Var "FdSp")) "being"   ($#l1_parsp_1 :::"FanodesSp":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "r")) "," (Set (Var "s")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "FdSp"))  "st" (Bool (Bool (Set (Var "a")) "," (Set (Var "b"))  ($#r3_parsp_2 :::"congr"::: )  (Set (Var "c")) "," (Set (Var "d"))) & (Bool (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c"))  ($#r1_parsp_2 :::"is_collinear"::: )  ) & (Bool   ($#r2_parsp_2 :::"parallelogram"::: )  (Set (Var "r")) "," (Set (Var "s")) "," (Set (Var "a")) "," (Set (Var "b")))) "holds"  (Bool   ($#r2_parsp_2 :::"parallelogram"::: )  (Set (Var "r")) "," (Set (Var "s")) "," (Set (Var "c")) "," (Set (Var "d"))))) ; 
 
theorem :: PARSP_2:53 (Bool  "for" (Set (Var "FdSp")) "being"   ($#l1_parsp_1 :::"FanodesSp":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "FdSp"))  "st" (Bool (Bool (Set (Var "a")) "," (Set (Var "b"))  ($#r3_parsp_2 :::"congr"::: )  (Set (Var "c")) "," (Set (Var "x"))) & (Bool (Set (Var "a")) "," (Set (Var "b"))  ($#r3_parsp_2 :::"congr"::: )  (Set (Var "c")) "," (Set (Var "y")))) "holds"  (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set (Var "y"))))) ; 
 
theorem :: PARSP_2:54 (Bool  "for" (Set (Var "FdSp")) "being"   ($#l1_parsp_1 :::"FanodesSp":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "FdSp")) (Bool  "ex" (Set (Var "d")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "FdSp")) "st" (Bool (Set (Var "a")) "," (Set (Var "b"))  ($#r3_parsp_2 :::"congr"::: )  (Set (Var "c")) "," (Set (Var "d")))))) ; 
 
theorem :: PARSP_2:55 (Bool  "for" (Set (Var "FdSp")) "being"   ($#l1_parsp_1 :::"FanodesSp":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "FdSp")) "holds"  (Bool (Set (Var "a")) "," (Set (Var "b"))  ($#r3_parsp_2 :::"congr"::: )  (Set (Var "a")) "," (Set (Var "b"))))) ; 
 
theorem :: PARSP_2:56 (Bool  "for" (Set (Var "FdSp")) "being"   ($#l1_parsp_1 :::"FanodesSp":::)  (Bool  "for" (Set (Var "r")) "," (Set (Var "s")) "," (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "FdSp"))  "st" (Bool (Bool (Set (Var "r")) "," (Set (Var "s"))  ($#r3_parsp_2 :::"congr"::: )  (Set (Var "a")) "," (Set (Var "b"))) & (Bool (Set (Var "r")) "," (Set (Var "s"))  ($#r3_parsp_2 :::"congr"::: )  (Set (Var "c")) "," (Set (Var "d")))) "holds"  (Bool (Set (Var "a")) "," (Set (Var "b"))  ($#r3_parsp_2 :::"congr"::: )  (Set (Var "c")) "," (Set (Var "d"))))) ; 
 
theorem :: PARSP_2:57 (Bool  "for" (Set (Var "FdSp")) "being"   ($#l1_parsp_1 :::"FanodesSp":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "FdSp"))  "st" (Bool (Bool (Set (Var "a")) "," (Set (Var "b"))  ($#r3_parsp_2 :::"congr"::: )  (Set (Var "c")) "," (Set (Var "d")))) "holds"  (Bool (Set (Var "c")) "," (Set (Var "d"))  ($#r3_parsp_2 :::"congr"::: )  (Set (Var "a")) "," (Set (Var "b"))))) ; 
 
theorem :: PARSP_2:58 (Bool  "for" (Set (Var "FdSp")) "being"   ($#l1_parsp_1 :::"FanodesSp":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "FdSp"))  "st" (Bool (Bool (Set (Var "a")) "," (Set (Var "b"))  ($#r3_parsp_2 :::"congr"::: )  (Set (Var "c")) "," (Set (Var "d")))) "holds"  (Bool (Set (Var "b")) "," (Set (Var "a"))  ($#r3_parsp_2 :::"congr"::: )  (Set (Var "d")) "," (Set (Var "c"))))) ;