:: SYMSP_1  semantic presentation begin  


definitionlet "F" be   ($#l6_algstr_0 :::"Field":::); attr "c2" is  :::"strict"::: ; struct  :::"SymStr":::  "over" "F" ->    ($#l1_orders_2 :::"RelStr"::: )   ","    ($#l1_vectsp_1 :::"VectSpStr"::: )   "over" "F"; aggr :::"SymStr":::(# :::"carrier":::, :::"addF":::, :::"ZeroF":::, :::"lmult":::, :::"InternalRel"::: #) ->    ($#l1_symsp_1 :::"SymStr"::: )   "over" "F"; end; registrationlet "F" be   ($#l6_algstr_0 :::"Field":::); 
cluster  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   for    ($#l1_symsp_1 :::"SymStr"::: )   "over" "F"; 
end; notationlet "F" be   ($#l6_algstr_0 :::"Field":::); let "S" be    ($#l1_symsp_1 :::"SymStr"::: )   "over" (Set (Const "F")); let "a", "b" be   ($#m1_subset_1 :::"Element":::) "of" (Set (Const "S")); synonym "a" :::"_|_"::: "b" for "S" :::"<="::: "a"; end; registrationlet "F" be   ($#l6_algstr_0 :::"Field":::); let "X" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  ; let "md" be   ($#m1_subset_1 :::"BinOp":::) "of" (Set (Const "X")); let "o" be    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Const "X")); let "mF" be   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Const "F"))) "," (Set (Const "X")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set (Const "X")); let "mo" be   ($#m1_subset_1 :::"Relation":::) "of" (Set (Const "X")); 
cluster (Set   ($#g1_symsp_1 :::"SymStr"::: )  "(#"  "X" "," "md" "," "o" "," "mF" "," "mo" "#)" ) ->  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )  ; 
end; registrationlet "F" be   ($#l6_algstr_0 :::"Field":::); 
cluster  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v13_algstr_0 :::"right_complementable"::: )     ($#v2_rlvect_1 :::"Abelian"::: )     ($#v3_rlvect_1 :::"add-associative"::: )     ($#v4_rlvect_1 :::"right_zeroed"::: )    for    ($#l1_symsp_1 :::"SymStr"::: )   "over" "F"; 
end; definitionlet "F" be   ($#l6_algstr_0 :::"Field":::); let "IT" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v13_algstr_0 :::"right_complementable"::: )     ($#v2_rlvect_1 :::"Abelian"::: )     ($#v3_rlvect_1 :::"add-associative"::: )     ($#v4_rlvect_1 :::"right_zeroed"::: )     ($#l1_symsp_1 :::"SymStr"::: )   "over" (Set (Const "F")); attr "IT" is  :::"SymSp-like":::  means :: SYMSP_1:def 1 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" "IT"  (Bool  "for" (Set (Var "l")) "being"   ($#m1_subset_1 :::"Element":::) "of" "F" "holds"   (Bool  "("   "("  (Bool (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k4_struct_0 :::"0."::: )  "IT"))) "implies" (Bool  "ex" (Set (Var "y")) "being"   ($#m1_subset_1 :::"Element":::) "of" "IT" "st" (Bool (Bool  "not" (Set (Var "a"))  ($#r1_orders_2 :::"_|_"::: )  )))  ")"  &  "("  (Bool (Bool (Set (Var "b"))  ($#r1_orders_2 :::"_|_"::: )  )) "implies" (Bool (Set (Var "b"))  ($#r1_orders_2 :::"_|_"::: )  )  ")"  &  "("  (Bool (Bool (Set (Var "a"))  ($#r1_orders_2 :::"_|_"::: )  ) & (Bool (Set (Var "a"))  ($#r1_orders_2 :::"_|_"::: )  )) "implies" (Bool (Set (Var "a"))  ($#r1_orders_2 :::"_|_"::: )  )  ")"  &  "("  (Bool (Bool (Bool  "not" (Set (Var "a"))  ($#r1_orders_2 :::"_|_"::: )  ))) "implies" (Bool  "ex" (Set (Var "k")) "being"   ($#m1_subset_1 :::"Element":::) "of" "F" "st" (Bool (Set (Var "a"))  ($#r1_orders_2 :::"_|_"::: )  ))  ")"  &  "("  (Bool (Bool (Set (Set (Var "b"))  ($#k3_rlvect_1 :::"+"::: )  (Set (Var "c")))  ($#r1_orders_2 :::"_|_"::: )  ) & (Bool (Set (Set (Var "c"))  ($#k3_rlvect_1 :::"+"::: )  (Set (Var "a")))  ($#r1_orders_2 :::"_|_"::: )  )) "implies" (Bool (Set (Set (Var "a"))  ($#k3_rlvect_1 :::"+"::: )  (Set (Var "b")))  ($#r1_orders_2 :::"_|_"::: )  )  ")"   ")" ))); end; 





:: deftheorem    defines :::"SymSp-like"::: SYMSP_1:def 1 :  (Bool  "for" (Set (Var "F")) "being"   ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "IT")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v13_algstr_0 :::"right_complementable"::: )     ($#v2_rlvect_1 :::"Abelian"::: )     ($#v3_rlvect_1 :::"add-associative"::: )     ($#v4_rlvect_1 :::"right_zeroed"::: )     ($#l1_symsp_1 :::"SymStr"::: )   "over" (Set (Var "F")) "holds"   (Bool  "("  (Bool (Set (Var "IT")) "is"   ($#v2_symsp_1 :::"SymSp-like"::: )  ) "iff" (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT"))  (Bool  "for" (Set (Var "l")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "F")) "holds"   (Bool  "("   "("  (Bool (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k4_struct_0 :::"0."::: )  (Set (Var "IT"))))) "implies" (Bool  "ex" (Set (Var "y")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT")) "st" (Bool (Bool  "not" (Set (Var "a"))  ($#r1_orders_2 :::"_|_"::: )  )))  ")"  &  "("  (Bool (Bool (Set (Var "b"))  ($#r1_orders_2 :::"_|_"::: )  )) "implies" (Bool (Set (Var "b"))  ($#r1_orders_2 :::"_|_"::: )  )  ")"  &  "("  (Bool (Bool (Set (Var "a"))  ($#r1_orders_2 :::"_|_"::: )  ) & (Bool (Set (Var "a"))  ($#r1_orders_2 :::"_|_"::: )  )) "implies" (Bool (Set (Var "a"))  ($#r1_orders_2 :::"_|_"::: )  )  ")"  &  "("  (Bool (Bool (Bool  "not" (Set (Var "a"))  ($#r1_orders_2 :::"_|_"::: )  ))) "implies" (Bool  "ex" (Set (Var "k")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "F")) "st" (Bool (Set (Var "a"))  ($#r1_orders_2 :::"_|_"::: )  ))  ")"  &  "("  (Bool (Bool (Set (Set (Var "b"))  ($#k3_rlvect_1 :::"+"::: )  (Set (Var "c")))  ($#r1_orders_2 :::"_|_"::: )  ) & (Bool (Set (Set (Var "c"))  ($#k3_rlvect_1 :::"+"::: )  (Set (Var "a")))  ($#r1_orders_2 :::"_|_"::: )  )) "implies" (Bool (Set (Set (Var "a"))  ($#k3_rlvect_1 :::"+"::: )  (Set (Var "b")))  ($#r1_orders_2 :::"_|_"::: )  )  ")"   ")" )))  ")" ))); 
 registrationlet "F" be   ($#l6_algstr_0 :::"Field":::); 
cluster  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v13_algstr_0 :::"right_complementable"::: )     ($#v2_rlvect_1 :::"Abelian"::: )     ($#v3_rlvect_1 :::"add-associative"::: )     ($#v4_rlvect_1 :::"right_zeroed"::: )     ($#v8_vectsp_1 :::"vector-distributive"::: )     ($#v9_vectsp_1 :::"scalar-distributive"::: )     ($#v10_vectsp_1 :::"scalar-associative"::: )     ($#v11_vectsp_1 :::"scalar-unital"::: )     ($#v1_symsp_1 :::"strict"::: )     ($#v2_symsp_1 :::"SymSp-like"::: )    for    ($#l1_symsp_1 :::"SymStr"::: )   "over" "F"; 
end; definitionlet "F" be   ($#l6_algstr_0 :::"Field":::); mode SymSp of "F" is  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v13_algstr_0 :::"right_complementable"::: )     ($#v2_rlvect_1 :::"Abelian"::: )     ($#v3_rlvect_1 :::"add-associative"::: )     ($#v4_rlvect_1 :::"right_zeroed"::: )     ($#v8_vectsp_1 :::"vector-distributive"::: )     ($#v9_vectsp_1 :::"scalar-distributive"::: )     ($#v10_vectsp_1 :::"scalar-associative"::: )     ($#v11_vectsp_1 :::"scalar-unital"::: )     ($#v2_symsp_1 :::"SymSp-like"::: )     ($#l1_symsp_1 :::"SymStr"::: )   "over" "F"; end; 






















theorem :: SYMSP_1:1 (Bool  "for" (Set (Var "F")) "being"   ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "S")) "being"   ($#l1_symsp_1 :::"SymSp":::) "of" (Set (Var "F"))  (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) "holds"  (Bool (Set (Var "a"))  ($#r1_orders_2 :::"_|_"::: )  )))) ; 
 
theorem :: SYMSP_1:2 (Bool  "for" (Set (Var "F")) "being"   ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "S")) "being"   ($#l1_symsp_1 :::"SymSp":::) "of" (Set (Var "F"))  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S"))  "st" (Bool (Bool (Set (Var "b"))  ($#r1_orders_2 :::"_|_"::: )  )) "holds"  (Bool (Set (Var "a"))  ($#r1_orders_2 :::"_|_"::: )  )))) ; 
 
theorem :: SYMSP_1:3 (Bool  "for" (Set (Var "F")) "being"   ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "S")) "being"   ($#l1_symsp_1 :::"SymSp":::) "of" (Set (Var "F"))  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S"))  "st" (Bool (Bool (Bool  "not" (Set (Var "b"))  ($#r1_orders_2 :::"_|_"::: )  )) & (Bool (Set (Var "b"))  ($#r1_orders_2 :::"_|_"::: )  )) "holds"  (Bool  "not" (Bool (Set (Var "b"))  ($#r1_orders_2 :::"_|_"::: )  ))))) ; 
 
theorem :: SYMSP_1:4 (Bool  "for" (Set (Var "F")) "being"   ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "S")) "being"   ($#l1_symsp_1 :::"SymSp":::) "of" (Set (Var "F"))  (Bool  "for" (Set (Var "b")) "," (Set (Var "a")) "," (Set (Var "c")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S"))  "st" (Bool (Bool (Bool  "not" (Set (Var "a"))  ($#r1_orders_2 :::"_|_"::: )  )) & (Bool (Set (Var "a"))  ($#r1_orders_2 :::"_|_"::: )  )) "holds"  (Bool  "not" (Bool (Set (Var "a"))  ($#r1_orders_2 :::"_|_"::: )  ))))) ; 
 
theorem :: SYMSP_1:5 (Bool  "for" (Set (Var "F")) "being"   ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "S")) "being"   ($#l1_symsp_1 :::"SymSp":::) "of" (Set (Var "F"))  (Bool  "for" (Set (Var "b")) "," (Set (Var "a")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S"))  (Bool  "for" (Set (Var "l")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "F"))  "st" (Bool (Bool (Bool  "not" (Set (Var "a"))  ($#r1_orders_2 :::"_|_"::: )  )) & (Bool (Bool  "not" (Set (Var "l"))  ($#r1_hidden :::"="::: )  (Set   ($#k4_struct_0 :::"0."::: )  (Set (Var "F")))))) "holds"  (Bool  "("  (Bool (Bool  "not" (Set (Var "a"))  ($#r1_orders_2 :::"_|_"::: )  )) & (Bool (Bool  "not" (Set (Set (Var "l"))  ($#k4_vectsp_1 :::"*"::: )  (Set (Var "a")))  ($#r1_orders_2 :::"_|_"::: )  ))  ")" ))))) ; 
 
theorem :: SYMSP_1:6 (Bool  "for" (Set (Var "F")) "being"   ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "S")) "being"   ($#l1_symsp_1 :::"SymSp":::) "of" (Set (Var "F"))  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S"))  "st" (Bool (Bool (Set (Var "b"))  ($#r1_orders_2 :::"_|_"::: )  )) "holds"  (Bool (Set (Var "b"))  ($#r1_orders_2 :::"_|_"::: )  )))) ; 
 
theorem :: SYMSP_1:7 (Bool  "for" (Set (Var "F")) "being"   ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "S")) "being"   ($#l1_symsp_1 :::"SymSp":::) "of" (Set (Var "F"))  (Bool  "for" (Set (Var "a")) "," (Set (Var "c")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S"))  "holds"  (Bool  "("  (Bool (Set (Var "c"))  ($#r1_orders_2 :::"_|_"::: )  ) "or"  "not" (Bool (Set (Var "c"))  ($#r1_orders_2 :::"_|_"::: )  ) "or"  "not" (Bool (Set (Var "c"))  ($#r1_orders_2 :::"_|_"::: )  )  ")" )))) ; 
 
theorem :: SYMSP_1:8 (Bool  "for" (Set (Var "F")) "being"   ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "S")) "being"   ($#l1_symsp_1 :::"SymSp":::) "of" (Set (Var "F"))  (Bool  "for" (Set (Var "a9")) "," (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "b9")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S"))  "st" (Bool (Bool (Bool  "not" (Set (Var "a"))  ($#r1_orders_2 :::"_|_"::: )  )) & (Bool (Set (Var "b"))  ($#r1_orders_2 :::"_|_"::: )  ) & (Bool (Bool  "not" (Set (Var "b"))  ($#r1_orders_2 :::"_|_"::: )  )) & (Bool (Set (Var "a"))  ($#r1_orders_2 :::"_|_"::: )  )) "holds"  (Bool  "("  (Bool (Bool  "not" (Set (Var "a"))  ($#r1_orders_2 :::"_|_"::: )  )) & (Bool (Bool  "not" (Set (Var "b"))  ($#r1_orders_2 :::"_|_"::: )  ))  ")" )))) ; 
 
theorem :: SYMSP_1:9 (Bool  "for" (Set (Var "F")) "being"   ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "S")) "being"   ($#l1_symsp_1 :::"SymSp":::) "of" (Set (Var "F"))  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S"))  "st" (Bool (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k4_struct_0 :::"0."::: )  (Set (Var "S")))) & (Bool (Set (Var "b"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k4_struct_0 :::"0."::: )  (Set (Var "S"))))) "holds"  (Bool  "ex" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) "st"  (Bool  "("  (Bool (Bool  "not" (Set (Var "a"))  ($#r1_orders_2 :::"_|_"::: )  )) & (Bool (Bool  "not" (Set (Var "b"))  ($#r1_orders_2 :::"_|_"::: )  ))  ")" ))))) ; 
 
theorem :: SYMSP_1:10 (Bool  "for" (Set (Var "F")) "being"   ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "S")) "being"   ($#l1_symsp_1 :::"SymSp":::) "of" (Set (Var "F"))  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S"))  "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 "a"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k4_struct_0 :::"0."::: )  (Set (Var "S")))) & (Bool (Set (Var "b"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k4_struct_0 :::"0."::: )  (Set (Var "S")))) & (Bool (Set (Var "c"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k4_struct_0 :::"0."::: )  (Set (Var "S"))))) "holds"  (Bool  "ex" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) "st"  (Bool  "("  (Bool (Bool  "not" (Set (Var "a"))  ($#r1_orders_2 :::"_|_"::: )  )) & (Bool (Bool  "not" (Set (Var "b"))  ($#r1_orders_2 :::"_|_"::: )  )) & (Bool (Bool  "not" (Set (Var "c"))  ($#r1_orders_2 :::"_|_"::: )  ))  ")" ))))) ; 
 
theorem :: SYMSP_1:11 (Bool  "for" (Set (Var "F")) "being"   ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "S")) "being"   ($#l1_symsp_1 :::"SymSp":::) "of" (Set (Var "F"))  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "d")) "," (Set (Var "c")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S"))  "st" (Bool (Bool (Set (Var "d"))  ($#r1_orders_2 :::"_|_"::: )  ) & (Bool (Set (Var "d"))  ($#r1_orders_2 :::"_|_"::: )  )) "holds"  (Bool (Set (Var "d"))  ($#r1_orders_2 :::"_|_"::: )  )))) ; 
 
theorem :: SYMSP_1:12 (Bool  "for" (Set (Var "F")) "being"   ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "S")) "being"   ($#l1_symsp_1 :::"SymSp":::) "of" (Set (Var "F"))  (Bool  "for" (Set (Var "b")) "," (Set (Var "a")) "," (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S"))  (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"))  ($#r1_orders_2 :::"_|_"::: )  )) & (Bool (Set (Var "a"))  ($#r1_orders_2 :::"_|_"::: )  ) & (Bool (Set (Var "a"))  ($#r1_orders_2 :::"_|_"::: )  )) "holds"  (Bool (Set (Var "k"))  ($#r1_hidden :::"="::: )  (Set (Var "l"))))))) ; 
 
theorem :: SYMSP_1:13 (Bool  "for" (Set (Var "F")) "being"   ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "S")) "being"   ($#l1_symsp_1 :::"SymSp":::) "of" (Set (Var "F"))  (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S"))  "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"))))) "holds"  (Bool (Set (Var "a"))  ($#r1_orders_2 :::"_|_"::: )  )))) ; 
 definitionlet "F" be   ($#l6_algstr_0 :::"Field":::); let "S" be   ($#l1_symsp_1 :::"SymSp":::) "of" (Set (Const "F")); let "a", "b", "x" be   ($#m1_subset_1 :::"Element":::) "of" (Set (Const "S")); assume 
(Bool (Bool  "not" (Set (Const "a"))  ($#r1_orders_2 :::"_|_"::: )  ))
 ; func  :::"ProJ":::  "(" "a" "," "b" "," "x" ")"  ->   ($#m1_subset_1 :::"Element":::) "of" "F" means :: SYMSP_1:def 2 (Bool  "for" (Set (Var "l")) "being"   ($#m1_subset_1 :::"Element":::) "of" "F"  "st" (Bool (Bool "a"  ($#r1_orders_2 :::"_|_"::: )  )) "holds"  (Bool it  ($#r1_hidden :::"="::: )  (Set (Var "l")))); end; 










:: deftheorem    defines :::"ProJ"::: SYMSP_1:def 2 :  (Bool  "for" (Set (Var "F")) "being"   ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "S")) "being"   ($#l1_symsp_1 :::"SymSp":::) "of" (Set (Var "F"))  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S"))  "st" (Bool (Bool (Bool  "not" (Set (Var "a"))  ($#r1_orders_2 :::"_|_"::: )  ))) "holds"  (Bool  "for" (Set (Var "b6")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "F")) "holds"   (Bool  "("  (Bool (Set (Var "b6"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_symsp_1 :::"ProJ"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "x")) ")" )) "iff" (Bool  "for" (Set (Var "l")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "F"))  "st" (Bool (Bool (Set (Var "a"))  ($#r1_orders_2 :::"_|_"::: )  )) "holds"  (Bool (Set (Var "b6"))  ($#r1_hidden :::"="::: )  (Set (Var "l"))))  ")" ))))); 
 
theorem :: SYMSP_1:14 (Bool  "for" (Set (Var "F")) "being"   ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "S")) "being"   ($#l1_symsp_1 :::"SymSp":::) "of" (Set (Var "F"))  (Bool  "for" (Set (Var "b")) "," (Set (Var "a")) "," (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S"))  "st" (Bool (Bool (Bool  "not" (Set (Var "a"))  ($#r1_orders_2 :::"_|_"::: )  ))) "holds"  (Bool (Set (Var "a"))  ($#r1_orders_2 :::"_|_"::: )  )))) ; 
 
theorem :: SYMSP_1:15 (Bool  "for" (Set (Var "F")) "being"   ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "S")) "being"   ($#l1_symsp_1 :::"SymSp":::) "of" (Set (Var "F"))  (Bool  "for" (Set (Var "b")) "," (Set (Var "a")) "," (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S"))  (Bool  "for" (Set (Var "l")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "F"))  "st" (Bool (Bool (Bool  "not" (Set (Var "a"))  ($#r1_orders_2 :::"_|_"::: )  ))) "holds"  (Bool (Set   ($#k1_symsp_1 :::"ProJ"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set  "(" (Set (Var "l"))  ($#k4_vectsp_1 :::"*"::: )  (Set (Var "x")) ")" ) ")" )  ($#r1_hidden :::"="::: )  (Set (Set (Var "l"))  ($#k8_group_1 :::"*"::: )  (Set  "("  ($#k1_symsp_1 :::"ProJ"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "x")) ")"  ")" ))))))) ; 
 
theorem :: SYMSP_1:16 (Bool  "for" (Set (Var "F")) "being"   ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "S")) "being"   ($#l1_symsp_1 :::"SymSp":::) "of" (Set (Var "F"))  (Bool  "for" (Set (Var "b")) "," (Set (Var "a")) "," (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S"))  "st" (Bool (Bool (Bool  "not" (Set (Var "a"))  ($#r1_orders_2 :::"_|_"::: )  ))) "holds"  (Bool (Set   ($#k1_symsp_1 :::"ProJ"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set  "(" (Set (Var "x"))  ($#k3_rlvect_1 :::"+"::: )  (Set (Var "y")) ")" ) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k1_symsp_1 :::"ProJ"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "x")) ")"  ")" )  ($#k3_rlvect_1 :::"+"::: )  (Set  "("  ($#k1_symsp_1 :::"ProJ"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "y")) ")"  ")" )))))) ; 
 
theorem :: SYMSP_1:17 (Bool  "for" (Set (Var "F")) "being"   ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "S")) "being"   ($#l1_symsp_1 :::"SymSp":::) "of" (Set (Var "F"))  (Bool  "for" (Set (Var "b")) "," (Set (Var "a")) "," (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S"))  (Bool  "for" (Set (Var "l")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "F"))  "st" (Bool (Bool (Bool  "not" (Set (Var "a"))  ($#r1_orders_2 :::"_|_"::: )  )) & (Bool (Set (Var "l"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k4_struct_0 :::"0."::: )  (Set (Var "F"))))) "holds"  (Bool (Set   ($#k1_symsp_1 :::"ProJ"::: )   "(" (Set (Var "a")) "," (Set  "(" (Set (Var "l"))  ($#k4_vectsp_1 :::"*"::: )  (Set (Var "b")) ")" ) "," (Set (Var "x")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "l"))  ($#k11_algstr_0 :::"""::: )  ")" )  ($#k8_group_1 :::"*"::: )  (Set  "("  ($#k1_symsp_1 :::"ProJ"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "x")) ")"  ")" ))))))) ; 
 
theorem :: SYMSP_1:18 (Bool  "for" (Set (Var "F")) "being"   ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "S")) "being"   ($#l1_symsp_1 :::"SymSp":::) "of" (Set (Var "F"))  (Bool  "for" (Set (Var "b")) "," (Set (Var "a")) "," (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S"))  (Bool  "for" (Set (Var "l")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "F"))  "st" (Bool (Bool (Bool  "not" (Set (Var "a"))  ($#r1_orders_2 :::"_|_"::: )  )) & (Bool (Set (Var "l"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k4_struct_0 :::"0."::: )  (Set (Var "F"))))) "holds"  (Bool (Set   ($#k1_symsp_1 :::"ProJ"::: )   "(" (Set  "(" (Set (Var "l"))  ($#k4_vectsp_1 :::"*"::: )  (Set (Var "a")) ")" ) "," (Set (Var "b")) "," (Set (Var "x")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k1_symsp_1 :::"ProJ"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "x")) ")" )))))) ; 
 
theorem :: SYMSP_1:19 (Bool  "for" (Set (Var "F")) "being"   ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "S")) "being"   ($#l1_symsp_1 :::"SymSp":::) "of" (Set (Var "F"))  (Bool  "for" (Set (Var "b")) "," (Set (Var "a")) "," (Set (Var "p")) "," (Set (Var "c")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S"))  "st" (Bool (Bool (Bool  "not" (Set (Var "a"))  ($#r1_orders_2 :::"_|_"::: )  )) & (Bool (Set (Var "a"))  ($#r1_orders_2 :::"_|_"::: )  )) "holds"  (Bool  "("  (Bool (Set   ($#k1_symsp_1 :::"ProJ"::: )   "(" (Set (Var "a")) "," (Set  "(" (Set (Var "b"))  ($#k3_rlvect_1 :::"+"::: )  (Set (Var "p")) ")" ) "," (Set (Var "c")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k1_symsp_1 :::"ProJ"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ")" )) & (Bool (Set   ($#k1_symsp_1 :::"ProJ"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set  "(" (Set (Var "c"))  ($#k3_rlvect_1 :::"+"::: )  (Set (Var "p")) ")" ) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k1_symsp_1 :::"ProJ"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ")" ))  ")" )))) ; 
 
theorem :: SYMSP_1:20 (Bool  "for" (Set (Var "F")) "being"   ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "S")) "being"   ($#l1_symsp_1 :::"SymSp":::) "of" (Set (Var "F"))  (Bool  "for" (Set (Var "b")) "," (Set (Var "a")) "," (Set (Var "p")) "," (Set (Var "c")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S"))  "st" (Bool (Bool (Bool  "not" (Set (Var "a"))  ($#r1_orders_2 :::"_|_"::: )  )) & (Bool (Set (Var "b"))  ($#r1_orders_2 :::"_|_"::: )  ) & (Bool (Set (Var "c"))  ($#r1_orders_2 :::"_|_"::: )  )) "holds"  (Bool (Set   ($#k1_symsp_1 :::"ProJ"::: )   "(" (Set  "(" (Set (Var "a"))  ($#k3_rlvect_1 :::"+"::: )  (Set (Var "p")) ")" ) "," (Set (Var "b")) "," (Set (Var "c")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k1_symsp_1 :::"ProJ"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ")" ))))) ; 
 
theorem :: SYMSP_1:21 (Bool  "for" (Set (Var "F")) "being"   ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "S")) "being"   ($#l1_symsp_1 :::"SymSp":::) "of" (Set (Var "F"))  (Bool  "for" (Set (Var "b")) "," (Set (Var "a")) "," (Set (Var "c")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S"))  "st" (Bool (Bool (Bool  "not" (Set (Var "a"))  ($#r1_orders_2 :::"_|_"::: )  )) & (Bool (Set (Var "a"))  ($#r1_orders_2 :::"_|_"::: )  )) "holds"  (Bool (Set   ($#k1_symsp_1 :::"ProJ"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k1_group_1 :::"1_"::: )  (Set (Var "F"))))))) ; 
 
theorem :: SYMSP_1:22 (Bool  "for" (Set (Var "F")) "being"   ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "S")) "being"   ($#l1_symsp_1 :::"SymSp":::) "of" (Set (Var "F"))  (Bool  "for" (Set (Var "b")) "," (Set (Var "a")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S"))  "st" (Bool (Bool (Bool  "not" (Set (Var "a"))  ($#r1_orders_2 :::"_|_"::: )  ))) "holds"  (Bool (Set   ($#k1_symsp_1 :::"ProJ"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "b")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k1_group_1 :::"1_"::: )  (Set (Var "F"))))))) ; 
 
theorem :: SYMSP_1:23 (Bool  "for" (Set (Var "F")) "being"   ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "S")) "being"   ($#l1_symsp_1 :::"SymSp":::) "of" (Set (Var "F"))  (Bool  "for" (Set (Var "b")) "," (Set (Var "a")) "," (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S"))  "st" (Bool (Bool (Bool  "not" (Set (Var "a"))  ($#r1_orders_2 :::"_|_"::: )  ))) "holds"  (Bool  "("  (Bool (Set (Var "a"))  ($#r1_orders_2 :::"_|_"::: )  ) "iff" (Bool (Set   ($#k1_symsp_1 :::"ProJ"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "x")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k4_struct_0 :::"0."::: )  (Set (Var "F"))))  ")" )))) ; 
 
theorem :: SYMSP_1:24 (Bool  "for" (Set (Var "F")) "being"   ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "S")) "being"   ($#l1_symsp_1 :::"SymSp":::) "of" (Set (Var "F"))  (Bool  "for" (Set (Var "b")) "," (Set (Var "a")) "," (Set (Var "q")) "," (Set (Var "p")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S"))  "st" (Bool (Bool (Bool  "not" (Set (Var "a"))  ($#r1_orders_2 :::"_|_"::: )  )) & (Bool (Bool  "not" (Set (Var "a"))  ($#r1_orders_2 :::"_|_"::: )  ))) "holds"  (Bool (Set (Set  "("  ($#k1_symsp_1 :::"ProJ"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "p")) ")"  ")" )  ($#k8_group_1 :::"*"::: )  (Set  "(" (Set  "("  ($#k1_symsp_1 :::"ProJ"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "q")) ")"  ")" )  ($#k11_algstr_0 :::"""::: )  ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k1_symsp_1 :::"ProJ"::: )   "(" (Set (Var "a")) "," (Set (Var "q")) "," (Set (Var "p")) ")" ))))) ; 
 
theorem :: SYMSP_1:25 (Bool  "for" (Set (Var "F")) "being"   ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "S")) "being"   ($#l1_symsp_1 :::"SymSp":::) "of" (Set (Var "F"))  (Bool  "for" (Set (Var "b")) "," (Set (Var "a")) "," (Set (Var "c")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S"))  "st" (Bool (Bool (Bool  "not" (Set (Var "a"))  ($#r1_orders_2 :::"_|_"::: )  )) & (Bool (Bool  "not" (Set (Var "a"))  ($#r1_orders_2 :::"_|_"::: )  ))) "holds"  (Bool (Set   ($#k1_symsp_1 :::"ProJ"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k1_symsp_1 :::"ProJ"::: )   "(" (Set (Var "a")) "," (Set (Var "c")) "," (Set (Var "b")) ")"  ")" )  ($#k11_algstr_0 :::"""::: )  ))))) ; 
 
theorem :: SYMSP_1:26 (Bool  "for" (Set (Var "F")) "being"   ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "S")) "being"   ($#l1_symsp_1 :::"SymSp":::) "of" (Set (Var "F"))  (Bool  "for" (Set (Var "b")) "," (Set (Var "a")) "," (Set (Var "c")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S"))  "st" (Bool (Bool (Bool  "not" (Set (Var "a"))  ($#r1_orders_2 :::"_|_"::: )  )) & (Bool (Set (Set (Var "c"))  ($#k3_rlvect_1 :::"+"::: )  (Set (Var "a")))  ($#r1_orders_2 :::"_|_"::: )  )) "holds"  (Bool (Set   ($#k1_symsp_1 :::"ProJ"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k1_symsp_1 :::"ProJ"::: )   "(" (Set (Var "c")) "," (Set (Var "b")) "," (Set (Var "a")) ")" ))))) ; 
 
theorem :: SYMSP_1:27 (Bool  "for" (Set (Var "F")) "being"   ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "S")) "being"   ($#l1_symsp_1 :::"SymSp":::) "of" (Set (Var "F"))  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S"))  "st" (Bool (Bool (Bool  "not" (Set (Var "b"))  ($#r1_orders_2 :::"_|_"::: )  )) & (Bool (Bool  "not" (Set (Var "b"))  ($#r1_orders_2 :::"_|_"::: )  ))) "holds"  (Bool (Set   ($#k1_symsp_1 :::"ProJ"::: )   "(" (Set (Var "c")) "," (Set (Var "b")) "," (Set (Var "a")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k4_algstr_0 :::"-"::: )  (Set  "(" (Set  "("  ($#k1_symsp_1 :::"ProJ"::: )   "(" (Set (Var "b")) "," (Set (Var "a")) "," (Set (Var "c")) ")"  ")" )  ($#k11_algstr_0 :::"""::: )  ")" ) ")" )  ($#k8_group_1 :::"*"::: )  (Set  "("  ($#k1_symsp_1 :::"ProJ"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ")"  ")" )))))) ; 
 
theorem :: SYMSP_1:28 (Bool  "for" (Set (Var "F")) "being"   ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "S")) "being"   ($#l1_symsp_1 :::"SymSp":::) "of" (Set (Var "F"))  (Bool  "for" (Set (Var "a")) "," (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S"))  "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 (Bool  "not" (Set (Var "p"))  ($#r1_orders_2 :::"_|_"::: )  )) & (Bool (Bool  "not" (Set (Var "q"))  ($#r1_orders_2 :::"_|_"::: )  )) & (Bool (Bool  "not" (Set (Var "q"))  ($#r1_orders_2 :::"_|_"::: )  ))) "holds"  (Bool (Set (Set  "("  ($#k1_symsp_1 :::"ProJ"::: )   "(" (Set (Var "a")) "," (Set (Var "p")) "," (Set (Var "q")) ")"  ")" )  ($#k8_group_1 :::"*"::: )  (Set  "("  ($#k1_symsp_1 :::"ProJ"::: )   "(" (Set (Var "b")) "," (Set (Var "q")) "," (Set (Var "p")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k1_symsp_1 :::"ProJ"::: )   "(" (Set (Var "p")) "," (Set (Var "a")) "," (Set (Var "b")) ")"  ")" )  ($#k8_group_1 :::"*"::: )  (Set  "("  ($#k1_symsp_1 :::"ProJ"::: )   "(" (Set (Var "q")) "," (Set (Var "b")) "," (Set (Var "a")) ")"  ")" )))))) ; 
 
theorem :: SYMSP_1:29 (Bool  "for" (Set (Var "F")) "being"   ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "S")) "being"   ($#l1_symsp_1 :::"SymSp":::) "of" (Set (Var "F"))  (Bool  "for" (Set (Var "p")) "," (Set (Var "a")) "," (Set (Var "x")) "," (Set (Var "q")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S"))  "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 (Bool  "not" (Set (Var "a"))  ($#r1_orders_2 :::"_|_"::: )  )) & (Bool (Bool  "not" (Set (Var "x"))  ($#r1_orders_2 :::"_|_"::: )  )) & (Bool (Bool  "not" (Set (Var "a"))  ($#r1_orders_2 :::"_|_"::: )  )) & (Bool (Bool  "not" (Set (Var "x"))  ($#r1_orders_2 :::"_|_"::: )  ))) "holds"  (Bool (Set (Set  "("  ($#k1_symsp_1 :::"ProJ"::: )   "(" (Set (Var "a")) "," (Set (Var "q")) "," (Set (Var "p")) ")"  ")" )  ($#k8_group_1 :::"*"::: )  (Set  "("  ($#k1_symsp_1 :::"ProJ"::: )   "(" (Set (Var "p")) "," (Set (Var "a")) "," (Set (Var "x")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k1_symsp_1 :::"ProJ"::: )   "(" (Set (Var "x")) "," (Set (Var "q")) "," (Set (Var "p")) ")"  ")" )  ($#k8_group_1 :::"*"::: )  (Set  "("  ($#k1_symsp_1 :::"ProJ"::: )   "(" (Set (Var "q")) "," (Set (Var "a")) "," (Set (Var "x")) ")"  ")" )))))) ; 
 
theorem :: SYMSP_1:30 (Bool  "for" (Set (Var "F")) "being"   ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "S")) "being"   ($#l1_symsp_1 :::"SymSp":::) "of" (Set (Var "F"))  (Bool  "for" (Set (Var "p")) "," (Set (Var "a")) "," (Set (Var "x")) "," (Set (Var "q")) "," (Set (Var "b")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S"))  "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 (Bool  "not" (Set (Var "a"))  ($#r1_orders_2 :::"_|_"::: )  )) & (Bool (Bool  "not" (Set (Var "x"))  ($#r1_orders_2 :::"_|_"::: )  )) & (Bool (Bool  "not" (Set (Var "a"))  ($#r1_orders_2 :::"_|_"::: )  )) & (Bool (Bool  "not" (Set (Var "x"))  ($#r1_orders_2 :::"_|_"::: )  )) & (Bool (Bool  "not" (Set (Var "a"))  ($#r1_orders_2 :::"_|_"::: )  ))) "holds"  (Bool (Set (Set  "(" (Set  "("  ($#k1_symsp_1 :::"ProJ"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "p")) ")"  ")" )  ($#k8_group_1 :::"*"::: )  (Set  "("  ($#k1_symsp_1 :::"ProJ"::: )   "(" (Set (Var "p")) "," (Set (Var "a")) "," (Set (Var "x")) ")"  ")" ) ")" )  ($#k8_group_1 :::"*"::: )  (Set  "("  ($#k1_symsp_1 :::"ProJ"::: )   "(" (Set (Var "x")) "," (Set (Var "p")) "," (Set (Var "y")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "("  ($#k1_symsp_1 :::"ProJ"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "q")) ")"  ")" )  ($#k8_group_1 :::"*"::: )  (Set  "("  ($#k1_symsp_1 :::"ProJ"::: )   "(" (Set (Var "q")) "," (Set (Var "a")) "," (Set (Var "x")) ")"  ")" ) ")" )  ($#k8_group_1 :::"*"::: )  (Set  "("  ($#k1_symsp_1 :::"ProJ"::: )   "(" (Set (Var "x")) "," (Set (Var "q")) "," (Set (Var "y")) ")"  ")" )))))) ; 
 
theorem :: SYMSP_1:31 (Bool  "for" (Set (Var "F")) "being"   ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "S")) "being"   ($#l1_symsp_1 :::"SymSp":::) "of" (Set (Var "F"))  (Bool  "for" (Set (Var "a")) "," (Set (Var "p")) "," (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S"))  "st" (Bool (Bool (Bool  "not" (Set (Var "p"))  ($#r1_orders_2 :::"_|_"::: )  )) & (Bool (Bool  "not" (Set (Var "p"))  ($#r1_orders_2 :::"_|_"::: )  )) & (Bool (Bool  "not" (Set (Var "p"))  ($#r1_orders_2 :::"_|_"::: )  ))) "holds"  (Bool (Set (Set  "("  ($#k1_symsp_1 :::"ProJ"::: )   "(" (Set (Var "p")) "," (Set (Var "a")) "," (Set (Var "x")) ")"  ")" )  ($#k8_group_1 :::"*"::: )  (Set  "("  ($#k1_symsp_1 :::"ProJ"::: )   "(" (Set (Var "x")) "," (Set (Var "p")) "," (Set (Var "y")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k4_algstr_0 :::"-"::: )  (Set  "("  ($#k1_symsp_1 :::"ProJ"::: )   "(" (Set (Var "p")) "," (Set (Var "a")) "," (Set (Var "y")) ")"  ")" ) ")" )  ($#k8_group_1 :::"*"::: )  (Set  "("  ($#k1_symsp_1 :::"ProJ"::: )   "(" (Set (Var "y")) "," (Set (Var "p")) "," (Set (Var "x")) ")"  ")" )))))) ; 
 definitionlet "F" be   ($#l6_algstr_0 :::"Field":::); let "S" be   ($#l1_symsp_1 :::"SymSp":::) "of" (Set (Const "F")); let "x", "y", "a", "b" be   ($#m1_subset_1 :::"Element":::) "of" (Set (Const "S")); assume 
(Bool  "("  (Bool (Bool  "not" (Set (Const "a"))  ($#r1_orders_2 :::"_|_"::: )  )) & (Bool (Set (Set  "("  ($#k1_group_1 :::"1_"::: )  (Set (Const "F")) ")" )  ($#k3_rlvect_1 :::"+"::: )  (Set  "("  ($#k1_group_1 :::"1_"::: )  (Set (Const "F")) ")" ))  ($#r1_hidden :::"<>"::: )  (Set   ($#k4_struct_0 :::"0."::: )  (Set (Const "F"))))  ")" )
 ; func  :::"PProJ":::  "(" "a" "," "b" "," "x" "," "y" ")"  ->   ($#m1_subset_1 :::"Element":::) "of" "F" means :: SYMSP_1:def 3 (Bool  "for" (Set (Var "q")) "being"   ($#m1_subset_1 :::"Element":::) "of" "S"  "st" (Bool (Bool (Bool  "not" "a"  ($#r1_orders_2 :::"_|_"::: )  )) & (Bool (Bool  "not" "x"  ($#r1_orders_2 :::"_|_"::: )  ))) "holds"  (Bool it  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "("  ($#k1_symsp_1 :::"ProJ"::: )   "(" "a" "," "b" "," (Set (Var "q")) ")"  ")" )  ($#k8_group_1 :::"*"::: )  (Set  "("  ($#k1_symsp_1 :::"ProJ"::: )   "(" (Set (Var "q")) "," "a" "," "x" ")"  ")" ) ")" )  ($#k8_group_1 :::"*"::: )  (Set  "("  ($#k1_symsp_1 :::"ProJ"::: )   "(" "x" "," (Set (Var "q")) "," "y" ")"  ")" )))) if (Bool  "ex" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Element":::) "of" "S" "st"  (Bool  "("  (Bool (Bool  "not" "a"  ($#r1_orders_2 :::"_|_"::: )  )) & (Bool (Bool  "not" "x"  ($#r1_orders_2 :::"_|_"::: )  ))  ")" ))  otherwise (Bool it  ($#r1_hidden :::"="::: )  (Set   ($#k4_struct_0 :::"0."::: )  "F")); end; 











:: deftheorem    defines :::"PProJ"::: SYMSP_1:def 3 :  (Bool  "for" (Set (Var "F")) "being"   ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "S")) "being"   ($#l1_symsp_1 :::"SymSp":::) "of" (Set (Var "F"))  (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S"))  "st" (Bool (Bool (Bool  "not" (Set (Var "a"))  ($#r1_orders_2 :::"_|_"::: )  )) & (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"))))) "holds"  (Bool  "for" (Set (Var "b7")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "F")) "holds"   (Bool  "("   "("  (Bool (Bool  "ex" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) "st"  (Bool  "("  (Bool (Bool  "not" (Set (Var "a"))  ($#r1_orders_2 :::"_|_"::: )  )) & (Bool (Bool  "not" (Set (Var "x"))  ($#r1_orders_2 :::"_|_"::: )  ))  ")" ))) "implies" (Bool  "("  (Bool (Set (Var "b7"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_symsp_1 :::"PProJ"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "x")) "," (Set (Var "y")) ")" )) "iff" (Bool  "for" (Set (Var "q")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S"))  "st" (Bool (Bool (Bool  "not" (Set (Var "a"))  ($#r1_orders_2 :::"_|_"::: )  )) & (Bool (Bool  "not" (Set (Var "x"))  ($#r1_orders_2 :::"_|_"::: )  ))) "holds"  (Bool (Set (Var "b7"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "("  ($#k1_symsp_1 :::"ProJ"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "q")) ")"  ")" )  ($#k8_group_1 :::"*"::: )  (Set  "("  ($#k1_symsp_1 :::"ProJ"::: )   "(" (Set (Var "q")) "," (Set (Var "a")) "," (Set (Var "x")) ")"  ")" ) ")" )  ($#k8_group_1 :::"*"::: )  (Set  "("  ($#k1_symsp_1 :::"ProJ"::: )   "(" (Set (Var "x")) "," (Set (Var "q")) "," (Set (Var "y")) ")"  ")" ))))  ")" )  ")"  &  "("  (Bool (Bool  "("   "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S"))  "holds"  (Bool  "("  (Bool (Set (Var "a"))  ($#r1_orders_2 :::"_|_"::: )  ) "or" (Bool (Set (Var "x"))  ($#r1_orders_2 :::"_|_"::: )  )  ")" )  ")" )) "implies" (Bool  "("  (Bool (Set (Var "b7"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_symsp_1 :::"PProJ"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "x")) "," (Set (Var "y")) ")" )) "iff" (Bool (Set (Var "b7"))  ($#r1_hidden :::"="::: )  (Set   ($#k4_struct_0 :::"0."::: )  (Set (Var "F"))))  ")" )  ")"   ")" ))))); 
 
theorem :: SYMSP_1:32 (Bool  "for" (Set (Var "F")) "being"   ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "S")) "being"   ($#l1_symsp_1 :::"SymSp":::) "of" (Set (Var "F"))  (Bool  "for" (Set (Var "b")) "," (Set (Var "a")) "," (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S"))  "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 (Bool  "not" (Set (Var "a"))  ($#r1_orders_2 :::"_|_"::: )  )) & (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set   ($#k4_struct_0 :::"0."::: )  (Set (Var "S"))))) "holds"  (Bool (Set   ($#k2_symsp_1 :::"PProJ"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "x")) "," (Set (Var "y")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k4_struct_0 :::"0."::: )  (Set (Var "F"))))))) ; 
 
theorem :: SYMSP_1:33 (Bool  "for" (Set (Var "F")) "being"   ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "S")) "being"   ($#l1_symsp_1 :::"SymSp":::) "of" (Set (Var "F"))  (Bool  "for" (Set (Var "b")) "," (Set (Var "a")) "," (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S"))  "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 (Bool  "not" (Set (Var "a"))  ($#r1_orders_2 :::"_|_"::: )  ))) "holds"  (Bool  "("  (Bool (Set   ($#k2_symsp_1 :::"PProJ"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "x")) "," (Set (Var "y")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k4_struct_0 :::"0."::: )  (Set (Var "F")))) "iff" (Bool (Set (Var "x"))  ($#r1_orders_2 :::"_|_"::: )  )  ")" )))) ; 
 
theorem :: SYMSP_1:34 (Bool  "for" (Set (Var "F")) "being"   ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "S")) "being"   ($#l1_symsp_1 :::"SymSp":::) "of" (Set (Var "F"))  (Bool  "for" (Set (Var "b")) "," (Set (Var "a")) "," (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S"))  "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 (Bool  "not" (Set (Var "a"))  ($#r1_orders_2 :::"_|_"::: )  ))) "holds"  (Bool (Set   ($#k2_symsp_1 :::"PProJ"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "x")) "," (Set (Var "y")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k4_algstr_0 :::"-"::: )  (Set  "("  ($#k2_symsp_1 :::"PProJ"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "y")) "," (Set (Var "x")) ")"  ")" )))))) ; 
 
theorem :: SYMSP_1:35 (Bool  "for" (Set (Var "F")) "being"   ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "S")) "being"   ($#l1_symsp_1 :::"SymSp":::) "of" (Set (Var "F"))  (Bool  "for" (Set (Var "b")) "," (Set (Var "a")) "," (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S"))  (Bool  "for" (Set (Var "l")) "being"   ($#m1_subset_1 :::"Element":::) "of" (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 (Bool  "not" (Set (Var "a"))  ($#r1_orders_2 :::"_|_"::: )  ))) "holds"  (Bool (Set   ($#k2_symsp_1 :::"PProJ"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "x")) "," (Set  "(" (Set (Var "l"))  ($#k4_vectsp_1 :::"*"::: )  (Set (Var "y")) ")" ) ")" )  ($#r1_hidden :::"="::: )  (Set (Set (Var "l"))  ($#k8_group_1 :::"*"::: )  (Set  "("  ($#k2_symsp_1 :::"PProJ"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "x")) "," (Set (Var "y")) ")"  ")" ))))))) ; 
 
theorem :: SYMSP_1:36 (Bool  "for" (Set (Var "F")) "being"   ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "S")) "being"   ($#l1_symsp_1 :::"SymSp":::) "of" (Set (Var "F"))  (Bool  "for" (Set (Var "b")) "," (Set (Var "a")) "," (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S"))  "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 (Bool  "not" (Set (Var "a"))  ($#r1_orders_2 :::"_|_"::: )  ))) "holds"  (Bool (Set   ($#k2_symsp_1 :::"PProJ"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "x")) "," (Set  "(" (Set (Var "y"))  ($#k3_rlvect_1 :::"+"::: )  (Set (Var "z")) ")" ) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k2_symsp_1 :::"PProJ"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "x")) "," (Set (Var "y")) ")"  ")" )  ($#k3_rlvect_1 :::"+"::: )  (Set  "("  ($#k2_symsp_1 :::"PProJ"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "x")) "," (Set (Var "z")) ")"  ")" )))))) ;