:: ALGSTR_2  semantic presentation begin  


registration
cluster (Set   ($#k2_vectsp_1 :::"F_Real"::: )  ) ->   ($#v7_algstr_1 :::"multLoop_0-like"::: )   ; 
end; definitionlet "L" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v5_algstr_0 :::"left_add-cancelable"::: )     ($#v3_algstr_1 :::"add-right-invertible"::: )     ($#l2_algstr_0 :::"addLoopStr"::: )  ; let "a" be   ($#m1_subset_1 :::"Element":::) "of" (Set (Const "L")); func  :::"-"::: "a" ->   ($#m1_subset_1 :::"Element":::) "of" "L" means :: ALGSTR_2:def 1 (Bool (Set "a"  ($#k1_algstr_0 :::"+"::: )  it)  ($#r1_hidden :::"="::: )  (Set   ($#k4_struct_0 :::"0."::: )  "L")); end; 






:: deftheorem    defines :::"-"::: ALGSTR_2:def 1 :  (Bool  "for" (Set (Var "L")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v5_algstr_0 :::"left_add-cancelable"::: )     ($#v3_algstr_1 :::"add-right-invertible"::: )     ($#l2_algstr_0 :::"addLoopStr"::: )    (Bool  "for" (Set (Var "a")) "," (Set (Var "b3")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"   (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_algstr_2 :::"-"::: )  (Set (Var "a")))) "iff" (Bool (Set (Set (Var "a"))  ($#k1_algstr_0 :::"+"::: )  (Set (Var "b3")))  ($#r1_hidden :::"="::: )  (Set   ($#k4_struct_0 :::"0."::: )  (Set (Var "L"))))  ")" ))); 
 definitionlet "L" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v5_algstr_0 :::"left_add-cancelable"::: )     ($#v3_algstr_1 :::"add-right-invertible"::: )     ($#l2_algstr_0 :::"addLoopStr"::: )  ; let "a", "b" be   ($#m1_subset_1 :::"Element":::) "of" (Set (Const "L")); func "a" :::"-"::: "b" ->   ($#m1_subset_1 :::"Element":::) "of" "L" equals :: ALGSTR_2:def 2 (Set "a"  ($#k1_algstr_0 :::"+"::: )  (Set  "("  ($#k1_algstr_2 :::"-"::: )  "b" ")" )); end; 







:: deftheorem    defines :::"-"::: ALGSTR_2:def 2 :  (Bool  "for" (Set (Var "L")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v5_algstr_0 :::"left_add-cancelable"::: )     ($#v3_algstr_1 :::"add-right-invertible"::: )     ($#l2_algstr_0 :::"addLoopStr"::: )    (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set (Var "a"))  ($#k2_algstr_2 :::"-"::: )  (Set (Var "b")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k1_algstr_0 :::"+"::: )  (Set  "("  ($#k1_algstr_2 :::"-"::: )  (Set (Var "b")) ")" ))))); 
 registration
cluster  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#~v6_struct_0  "non"   ($#v6_struct_0 :::"degenerated"::: )   )    ($#v36_algstr_0 :::"strict"::: )     ($#v1_algstr_1 :::"left_zeroed"::: )     ($#v4_algstr_1 :::"Loop-like"::: )     ($#v7_algstr_1 :::"multLoop_0-like"::: )     ($#v2_rlvect_1 :::"Abelian"::: )     ($#v3_rlvect_1 :::"add-associative"::: )     ($#v4_rlvect_1 :::"right_zeroed"::: )     ($#v3_group_1 :::"associative"::: )     ($#v5_group_1 :::"commutative"::: )     ($#v4_vectsp_1 :::"well-unital"::: )     ($#v5_vectsp_1 :::"distributive"::: )    for    ($#l6_algstr_0 :::"doubleLoopStr"::: )  ; 
end; definitionmode doubleLoop is  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_algstr_1 :::"left_zeroed"::: )     ($#v4_algstr_1 :::"Loop-like"::: )     ($#v7_algstr_1 :::"multLoop_0-like"::: )     ($#v4_rlvect_1 :::"right_zeroed"::: )     ($#v4_vectsp_1 :::"well-unital"::: )     ($#l6_algstr_0 :::"doubleLoopStr"::: )  ; end; definitionmode leftQuasi-Field is  ($#~v6_struct_0  "non"   ($#v6_struct_0 :::"degenerated"::: )   )    ($#v2_rlvect_1 :::"Abelian"::: )     ($#v3_rlvect_1 :::"add-associative"::: )     ($#v1_vectsp_1 :::"right-distributive"::: )    ($#l6_algstr_0 :::"doubleLoop":::); end; 








theorem :: ALGSTR_2:1 (Bool  "for" (Set (Var "L")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l6_algstr_0 :::"doubleLoopStr"::: )   "holds"   (Bool  "("  (Bool (Set (Var "L")) "is"   ($#l6_algstr_0 :::"leftQuasi-Field":::)) "iff" (Bool  "("  (Bool  "("   "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set (Var "a"))  ($#k1_algstr_0 :::"+"::: )  (Set  "("  ($#k4_struct_0 :::"0."::: )  (Set (Var "L")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "a")))  ")" ) & (Bool  "("   "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) (Bool  "ex" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Set (Set (Var "a"))  ($#k1_algstr_0 :::"+"::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set   ($#k4_struct_0 :::"0."::: )  (Set (Var "L")))))  ")" ) & (Bool  "("   "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set  "(" (Set (Var "a"))  ($#k1_algstr_0 :::"+"::: )  (Set (Var "b")) ")" )  ($#k1_algstr_0 :::"+"::: )  (Set (Var "c")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k1_algstr_0 :::"+"::: )  (Set  "(" (Set (Var "b"))  ($#k1_algstr_0 :::"+"::: )  (Set (Var "c")) ")" )))  ")" ) & (Bool  "("   "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set (Var "a"))  ($#k1_algstr_0 :::"+"::: )  (Set (Var "b")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "b"))  ($#k1_algstr_0 :::"+"::: )  (Set (Var "a"))))  ")" ) & (Bool (Set   ($#k4_struct_0 :::"0."::: )  (Set (Var "L")))  ($#r1_hidden :::"<>"::: )  (Set   ($#k5_struct_0 :::"1."::: )  (Set (Var "L")))) & (Bool  "("   "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set (Var "a"))  ($#k6_algstr_0 :::"*"::: )  (Set  "("  ($#k5_struct_0 :::"1."::: )  (Set (Var "L")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "a")))  ")" ) & (Bool  "("   "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set  "("  ($#k5_struct_0 :::"1."::: )  (Set (Var "L")) ")" )  ($#k6_algstr_0 :::"*"::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set (Var "a")))  ")" ) & (Bool  "("   "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L"))  "st" (Bool (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k4_struct_0 :::"0."::: )  (Set (Var "L"))))) "holds"  (Bool  "ex" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Set (Set (Var "a"))  ($#k6_algstr_0 :::"*"::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Var "b"))))  ")" ) & (Bool  "("   "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L"))  "st" (Bool (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k4_struct_0 :::"0."::: )  (Set (Var "L"))))) "holds"  (Bool  "ex" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Set (Set (Var "x"))  ($#k6_algstr_0 :::"*"::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set (Var "b"))))  ")" ) & (Bool  "("   "for" (Set (Var "a")) "," (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L"))  "st" (Bool (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k4_struct_0 :::"0."::: )  (Set (Var "L")))) & (Bool (Set (Set (Var "a"))  ($#k6_algstr_0 :::"*"::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k6_algstr_0 :::"*"::: )  (Set (Var "y"))))) "holds"  (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set (Var "y")))  ")" ) & (Bool  "("   "for" (Set (Var "a")) "," (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L"))  "st" (Bool (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k4_struct_0 :::"0."::: )  (Set (Var "L")))) & (Bool (Set (Set (Var "x"))  ($#k6_algstr_0 :::"*"::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "y"))  ($#k6_algstr_0 :::"*"::: )  (Set (Var "a"))))) "holds"  (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set (Var "y")))  ")" ) & (Bool  "("   "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set (Var "a"))  ($#k6_algstr_0 :::"*"::: )  (Set  "("  ($#k4_struct_0 :::"0."::: )  (Set (Var "L")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k4_struct_0 :::"0."::: )  (Set (Var "L"))))  ")" ) & (Bool  "("   "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set  "("  ($#k4_struct_0 :::"0."::: )  (Set (Var "L")) ")" )  ($#k6_algstr_0 :::"*"::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set   ($#k4_struct_0 :::"0."::: )  (Set (Var "L"))))  ")" ) & (Bool  "("   "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set (Var "a"))  ($#k6_algstr_0 :::"*"::: )  (Set  "(" (Set (Var "b"))  ($#k1_algstr_0 :::"+"::: )  (Set (Var "c")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "a"))  ($#k6_algstr_0 :::"*"::: )  (Set (Var "b")) ")" )  ($#k1_algstr_0 :::"+"::: )  (Set  "(" (Set (Var "a"))  ($#k6_algstr_0 :::"*"::: )  (Set (Var "c")) ")" )))  ")" )  ")" )  ")" )) ; 
 
theorem :: ALGSTR_2:2 (Bool  "for" (Set (Var "G")) "being"   ($#v2_rlvect_1 :::"Abelian"::: )     ($#v1_vectsp_1 :::"right-distributive"::: )    ($#l6_algstr_0 :::"doubleLoop":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds"  (Bool (Set (Set (Var "a"))  ($#k6_algstr_0 :::"*"::: )  (Set  "("  ($#k1_algstr_2 :::"-"::: )  (Set (Var "b")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k1_algstr_2 :::"-"::: )  (Set  "(" (Set (Var "a"))  ($#k6_algstr_0 :::"*"::: )  (Set (Var "b")) ")" ))))) ; 
 
theorem :: ALGSTR_2:3 (Bool  "for" (Set (Var "G")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v5_algstr_0 :::"left_add-cancelable"::: )     ($#v3_algstr_1 :::"add-right-invertible"::: )     ($#v2_rlvect_1 :::"Abelian"::: )     ($#l2_algstr_0 :::"addLoopStr"::: )    (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds"  (Bool (Set   ($#k1_algstr_2 :::"-"::: )  (Set  "("  ($#k1_algstr_2 :::"-"::: )  (Set (Var "a")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "a"))))) ; 
 
theorem :: ALGSTR_2:4 (Bool  "for" (Set (Var "G")) "being"   ($#v2_rlvect_1 :::"Abelian"::: )     ($#v1_vectsp_1 :::"right-distributive"::: )    ($#l6_algstr_0 :::"doubleLoop":::) "holds"  (Bool (Set (Set  "("  ($#k1_algstr_2 :::"-"::: )  (Set  "("  ($#k5_struct_0 :::"1."::: )  (Set (Var "G")) ")" ) ")" )  ($#k6_algstr_0 :::"*"::: )  (Set  "("  ($#k1_algstr_2 :::"-"::: )  (Set  "("  ($#k5_struct_0 :::"1."::: )  (Set (Var "G")) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k5_struct_0 :::"1."::: )  (Set (Var "G"))))) ; 
 
theorem :: ALGSTR_2:5 (Bool  "for" (Set (Var "G")) "being"   ($#v2_rlvect_1 :::"Abelian"::: )     ($#v1_vectsp_1 :::"right-distributive"::: )    ($#l6_algstr_0 :::"doubleLoop":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds"  (Bool (Set (Set (Var "a"))  ($#k6_algstr_0 :::"*"::: )  (Set  "(" (Set (Var "x"))  ($#k2_algstr_2 :::"-"::: )  (Set (Var "y")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "a"))  ($#k6_algstr_0 :::"*"::: )  (Set (Var "x")) ")" )  ($#k2_algstr_2 :::"-"::: )  (Set  "(" (Set (Var "a"))  ($#k6_algstr_0 :::"*"::: )  (Set (Var "y")) ")" ))))) ; 
 definitionmode rightQuasi-Field is  ($#~v6_struct_0  "non"   ($#v6_struct_0 :::"degenerated"::: )   )    ($#v2_rlvect_1 :::"Abelian"::: )     ($#v3_rlvect_1 :::"add-associative"::: )     ($#v2_vectsp_1 :::"left-distributive"::: )    ($#l6_algstr_0 :::"doubleLoop":::); end; 
theorem :: ALGSTR_2:6 (Bool  "for" (Set (Var "L")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l6_algstr_0 :::"doubleLoopStr"::: )   "holds"   (Bool  "("  (Bool (Set (Var "L")) "is"   ($#l6_algstr_0 :::"rightQuasi-Field":::)) "iff" (Bool  "("  (Bool  "("   "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set (Var "a"))  ($#k1_algstr_0 :::"+"::: )  (Set  "("  ($#k4_struct_0 :::"0."::: )  (Set (Var "L")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "a")))  ")" ) & (Bool  "("   "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) (Bool  "ex" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Set (Set (Var "a"))  ($#k1_algstr_0 :::"+"::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set   ($#k4_struct_0 :::"0."::: )  (Set (Var "L")))))  ")" ) & (Bool  "("   "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set  "(" (Set (Var "a"))  ($#k1_algstr_0 :::"+"::: )  (Set (Var "b")) ")" )  ($#k1_algstr_0 :::"+"::: )  (Set (Var "c")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k1_algstr_0 :::"+"::: )  (Set  "(" (Set (Var "b"))  ($#k1_algstr_0 :::"+"::: )  (Set (Var "c")) ")" )))  ")" ) & (Bool  "("   "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set (Var "a"))  ($#k1_algstr_0 :::"+"::: )  (Set (Var "b")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "b"))  ($#k1_algstr_0 :::"+"::: )  (Set (Var "a"))))  ")" ) & (Bool (Set   ($#k4_struct_0 :::"0."::: )  (Set (Var "L")))  ($#r1_hidden :::"<>"::: )  (Set   ($#k5_struct_0 :::"1."::: )  (Set (Var "L")))) & (Bool  "("   "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set (Var "a"))  ($#k6_algstr_0 :::"*"::: )  (Set  "("  ($#k5_struct_0 :::"1."::: )  (Set (Var "L")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "a")))  ")" ) & (Bool  "("   "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set  "("  ($#k5_struct_0 :::"1."::: )  (Set (Var "L")) ")" )  ($#k6_algstr_0 :::"*"::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set (Var "a")))  ")" ) & (Bool  "("   "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L"))  "st" (Bool (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k4_struct_0 :::"0."::: )  (Set (Var "L"))))) "holds"  (Bool  "ex" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Set (Set (Var "a"))  ($#k6_algstr_0 :::"*"::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Var "b"))))  ")" ) & (Bool  "("   "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L"))  "st" (Bool (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k4_struct_0 :::"0."::: )  (Set (Var "L"))))) "holds"  (Bool  "ex" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Set (Set (Var "x"))  ($#k6_algstr_0 :::"*"::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set (Var "b"))))  ")" ) & (Bool  "("   "for" (Set (Var "a")) "," (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L"))  "st" (Bool (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k4_struct_0 :::"0."::: )  (Set (Var "L")))) & (Bool (Set (Set (Var "a"))  ($#k6_algstr_0 :::"*"::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k6_algstr_0 :::"*"::: )  (Set (Var "y"))))) "holds"  (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set (Var "y")))  ")" ) & (Bool  "("   "for" (Set (Var "a")) "," (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L"))  "st" (Bool (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k4_struct_0 :::"0."::: )  (Set (Var "L")))) & (Bool (Set (Set (Var "x"))  ($#k6_algstr_0 :::"*"::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "y"))  ($#k6_algstr_0 :::"*"::: )  (Set (Var "a"))))) "holds"  (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set (Var "y")))  ")" ) & (Bool  "("   "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set (Var "a"))  ($#k6_algstr_0 :::"*"::: )  (Set  "("  ($#k4_struct_0 :::"0."::: )  (Set (Var "L")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k4_struct_0 :::"0."::: )  (Set (Var "L"))))  ")" ) & (Bool  "("   "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set  "("  ($#k4_struct_0 :::"0."::: )  (Set (Var "L")) ")" )  ($#k6_algstr_0 :::"*"::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set   ($#k4_struct_0 :::"0."::: )  (Set (Var "L"))))  ")" ) & (Bool  "("   "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set  "(" (Set (Var "b"))  ($#k1_algstr_0 :::"+"::: )  (Set (Var "c")) ")" )  ($#k6_algstr_0 :::"*"::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "b"))  ($#k6_algstr_0 :::"*"::: )  (Set (Var "a")) ")" )  ($#k1_algstr_0 :::"+"::: )  (Set  "(" (Set (Var "c"))  ($#k6_algstr_0 :::"*"::: )  (Set (Var "a")) ")" )))  ")" )  ")" )  ")" )) ; 
 









theorem :: ALGSTR_2:7 (Bool  "for" (Set (Var "G")) "being"   ($#v2_vectsp_1 :::"left-distributive"::: )    ($#l6_algstr_0 :::"doubleLoop":::)  (Bool  "for" (Set (Var "b")) "," (Set (Var "a")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds"  (Bool (Set (Set  "("  ($#k1_algstr_2 :::"-"::: )  (Set (Var "b")) ")" )  ($#k6_algstr_0 :::"*"::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_algstr_2 :::"-"::: )  (Set  "(" (Set (Var "b"))  ($#k6_algstr_0 :::"*"::: )  (Set (Var "a")) ")" ))))) ; 
 
theorem :: ALGSTR_2:8 (Bool  "for" (Set (Var "G")) "being"   ($#v2_rlvect_1 :::"Abelian"::: )     ($#v2_vectsp_1 :::"left-distributive"::: )    ($#l6_algstr_0 :::"doubleLoop":::) "holds"  (Bool (Set (Set  "("  ($#k1_algstr_2 :::"-"::: )  (Set  "("  ($#k5_struct_0 :::"1."::: )  (Set (Var "G")) ")" ) ")" )  ($#k6_algstr_0 :::"*"::: )  (Set  "("  ($#k1_algstr_2 :::"-"::: )  (Set  "("  ($#k5_struct_0 :::"1."::: )  (Set (Var "G")) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k5_struct_0 :::"1."::: )  (Set (Var "G"))))) ; 
 
theorem :: ALGSTR_2:9 (Bool  "for" (Set (Var "G")) "being"   ($#v2_vectsp_1 :::"left-distributive"::: )    ($#l6_algstr_0 :::"doubleLoop":::)  (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "a")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds"  (Bool (Set (Set  "(" (Set (Var "x"))  ($#k2_algstr_2 :::"-"::: )  (Set (Var "y")) ")" )  ($#k6_algstr_0 :::"*"::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "x"))  ($#k6_algstr_0 :::"*"::: )  (Set (Var "a")) ")" )  ($#k2_algstr_2 :::"-"::: )  (Set  "(" (Set (Var "y"))  ($#k6_algstr_0 :::"*"::: )  (Set (Var "a")) ")" ))))) ; 
 definitionmode doublesidedQuasi-Field is  ($#~v6_struct_0  "non"   ($#v6_struct_0 :::"degenerated"::: )   )    ($#v2_rlvect_1 :::"Abelian"::: )     ($#v3_rlvect_1 :::"add-associative"::: )     ($#v5_vectsp_1 :::"distributive"::: )    ($#l6_algstr_0 :::"doubleLoop":::); end; 








theorem :: ALGSTR_2:10 (Bool  "for" (Set (Var "L")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l6_algstr_0 :::"doubleLoopStr"::: )   "holds"   (Bool  "("  (Bool (Set (Var "L")) "is"   ($#l6_algstr_0 :::"doublesidedQuasi-Field":::)) "iff" (Bool  "("  (Bool  "("   "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set (Var "a"))  ($#k1_algstr_0 :::"+"::: )  (Set  "("  ($#k4_struct_0 :::"0."::: )  (Set (Var "L")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "a")))  ")" ) & (Bool  "("   "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) (Bool  "ex" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Set (Set (Var "a"))  ($#k1_algstr_0 :::"+"::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set   ($#k4_struct_0 :::"0."::: )  (Set (Var "L")))))  ")" ) & (Bool  "("   "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set  "(" (Set (Var "a"))  ($#k1_algstr_0 :::"+"::: )  (Set (Var "b")) ")" )  ($#k1_algstr_0 :::"+"::: )  (Set (Var "c")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k1_algstr_0 :::"+"::: )  (Set  "(" (Set (Var "b"))  ($#k1_algstr_0 :::"+"::: )  (Set (Var "c")) ")" )))  ")" ) & (Bool  "("   "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set (Var "a"))  ($#k1_algstr_0 :::"+"::: )  (Set (Var "b")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "b"))  ($#k1_algstr_0 :::"+"::: )  (Set (Var "a"))))  ")" ) & (Bool (Set   ($#k4_struct_0 :::"0."::: )  (Set (Var "L")))  ($#r1_hidden :::"<>"::: )  (Set   ($#k5_struct_0 :::"1."::: )  (Set (Var "L")))) & (Bool  "("   "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set (Var "a"))  ($#k6_algstr_0 :::"*"::: )  (Set  "("  ($#k5_struct_0 :::"1."::: )  (Set (Var "L")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "a")))  ")" ) & (Bool  "("   "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set  "("  ($#k5_struct_0 :::"1."::: )  (Set (Var "L")) ")" )  ($#k6_algstr_0 :::"*"::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set (Var "a")))  ")" ) & (Bool  "("   "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L"))  "st" (Bool (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k4_struct_0 :::"0."::: )  (Set (Var "L"))))) "holds"  (Bool  "ex" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Set (Set (Var "a"))  ($#k6_algstr_0 :::"*"::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Var "b"))))  ")" ) & (Bool  "("   "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L"))  "st" (Bool (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k4_struct_0 :::"0."::: )  (Set (Var "L"))))) "holds"  (Bool  "ex" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Set (Set (Var "x"))  ($#k6_algstr_0 :::"*"::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set (Var "b"))))  ")" ) & (Bool  "("   "for" (Set (Var "a")) "," (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L"))  "st" (Bool (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k4_struct_0 :::"0."::: )  (Set (Var "L")))) & (Bool (Set (Set (Var "a"))  ($#k6_algstr_0 :::"*"::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k6_algstr_0 :::"*"::: )  (Set (Var "y"))))) "holds"  (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set (Var "y")))  ")" ) & (Bool  "("   "for" (Set (Var "a")) "," (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L"))  "st" (Bool (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k4_struct_0 :::"0."::: )  (Set (Var "L")))) & (Bool (Set (Set (Var "x"))  ($#k6_algstr_0 :::"*"::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "y"))  ($#k6_algstr_0 :::"*"::: )  (Set (Var "a"))))) "holds"  (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set (Var "y")))  ")" ) & (Bool  "("   "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set (Var "a"))  ($#k6_algstr_0 :::"*"::: )  (Set  "("  ($#k4_struct_0 :::"0."::: )  (Set (Var "L")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k4_struct_0 :::"0."::: )  (Set (Var "L"))))  ")" ) & (Bool  "("   "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set  "("  ($#k4_struct_0 :::"0."::: )  (Set (Var "L")) ")" )  ($#k6_algstr_0 :::"*"::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set   ($#k4_struct_0 :::"0."::: )  (Set (Var "L"))))  ")" ) & (Bool  "("   "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set (Var "a"))  ($#k6_algstr_0 :::"*"::: )  (Set  "(" (Set (Var "b"))  ($#k1_algstr_0 :::"+"::: )  (Set (Var "c")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "a"))  ($#k6_algstr_0 :::"*"::: )  (Set (Var "b")) ")" )  ($#k1_algstr_0 :::"+"::: )  (Set  "(" (Set (Var "a"))  ($#k6_algstr_0 :::"*"::: )  (Set (Var "c")) ")" )))  ")" ) & (Bool  "("   "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set  "(" (Set (Var "b"))  ($#k1_algstr_0 :::"+"::: )  (Set (Var "c")) ")" )  ($#k6_algstr_0 :::"*"::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "b"))  ($#k6_algstr_0 :::"*"::: )  (Set (Var "a")) ")" )  ($#k1_algstr_0 :::"+"::: )  (Set  "(" (Set (Var "c"))  ($#k6_algstr_0 :::"*"::: )  (Set (Var "a")) ")" )))  ")" )  ")" )  ")" )) ; 
 definitionmode _Skew-Field is   ($#v3_group_1 :::"associative"::: )    ($#l6_algstr_0 :::"doublesidedQuasi-Field":::); end; 
theorem :: ALGSTR_2:11 (Bool  "for" (Set (Var "L")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l6_algstr_0 :::"doubleLoopStr"::: )   "holds"   (Bool  "("  (Bool (Set (Var "L")) "is"   ($#l6_algstr_0 :::"_Skew-Field":::)) "iff" (Bool  "("  (Bool  "("   "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set (Var "a"))  ($#k1_algstr_0 :::"+"::: )  (Set  "("  ($#k4_struct_0 :::"0."::: )  (Set (Var "L")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "a")))  ")" ) & (Bool  "("   "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) (Bool  "ex" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Set (Set (Var "a"))  ($#k1_algstr_0 :::"+"::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set   ($#k4_struct_0 :::"0."::: )  (Set (Var "L")))))  ")" ) & (Bool  "("   "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set  "(" (Set (Var "a"))  ($#k1_algstr_0 :::"+"::: )  (Set (Var "b")) ")" )  ($#k1_algstr_0 :::"+"::: )  (Set (Var "c")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k1_algstr_0 :::"+"::: )  (Set  "(" (Set (Var "b"))  ($#k1_algstr_0 :::"+"::: )  (Set (Var "c")) ")" )))  ")" ) & (Bool  "("   "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set (Var "a"))  ($#k1_algstr_0 :::"+"::: )  (Set (Var "b")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "b"))  ($#k1_algstr_0 :::"+"::: )  (Set (Var "a"))))  ")" ) & (Bool (Set   ($#k4_struct_0 :::"0."::: )  (Set (Var "L")))  ($#r1_hidden :::"<>"::: )  (Set   ($#k5_struct_0 :::"1."::: )  (Set (Var "L")))) & (Bool  "("   "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set (Var "a"))  ($#k6_algstr_0 :::"*"::: )  (Set  "("  ($#k5_struct_0 :::"1."::: )  (Set (Var "L")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "a")))  ")" ) & (Bool  "("   "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L"))  "st" (Bool (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k4_struct_0 :::"0."::: )  (Set (Var "L"))))) "holds"  (Bool  "ex" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Set (Set (Var "a"))  ($#k6_algstr_0 :::"*"::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set   ($#k5_struct_0 :::"1."::: )  (Set (Var "L")))))  ")" ) & (Bool  "("   "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set (Var "a"))  ($#k6_algstr_0 :::"*"::: )  (Set  "("  ($#k4_struct_0 :::"0."::: )  (Set (Var "L")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k4_struct_0 :::"0."::: )  (Set (Var "L"))))  ")" ) & (Bool  "("   "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set  "("  ($#k4_struct_0 :::"0."::: )  (Set (Var "L")) ")" )  ($#k6_algstr_0 :::"*"::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set   ($#k4_struct_0 :::"0."::: )  (Set (Var "L"))))  ")" ) & (Bool  "("   "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set  "(" (Set (Var "a"))  ($#k6_algstr_0 :::"*"::: )  (Set (Var "b")) ")" )  ($#k6_algstr_0 :::"*"::: )  (Set (Var "c")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k6_algstr_0 :::"*"::: )  (Set  "(" (Set (Var "b"))  ($#k6_algstr_0 :::"*"::: )  (Set (Var "c")) ")" )))  ")" ) & (Bool  "("   "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set (Var "a"))  ($#k6_algstr_0 :::"*"::: )  (Set  "(" (Set (Var "b"))  ($#k1_algstr_0 :::"+"::: )  (Set (Var "c")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "a"))  ($#k6_algstr_0 :::"*"::: )  (Set (Var "b")) ")" )  ($#k1_algstr_0 :::"+"::: )  (Set  "(" (Set (Var "a"))  ($#k6_algstr_0 :::"*"::: )  (Set (Var "c")) ")" )))  ")" ) & (Bool  "("   "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set  "(" (Set (Var "b"))  ($#k1_algstr_0 :::"+"::: )  (Set (Var "c")) ")" )  ($#k6_algstr_0 :::"*"::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "b"))  ($#k6_algstr_0 :::"*"::: )  (Set (Var "a")) ")" )  ($#k1_algstr_0 :::"+"::: )  (Set  "(" (Set (Var "c"))  ($#k6_algstr_0 :::"*"::: )  (Set (Var "a")) ")" )))  ")" )  ")" )  ")" )) ; 
 definitionmode _Field is   ($#v5_group_1 :::"commutative"::: )    ($#l6_algstr_0 :::"_Skew-Field":::); end; 
theorem :: ALGSTR_2:12 (Bool  "for" (Set (Var "L")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l6_algstr_0 :::"doubleLoopStr"::: )   "holds"   (Bool  "("  (Bool (Set (Var "L")) "is"   ($#l6_algstr_0 :::"_Field":::)) "iff" (Bool  "("  (Bool  "("   "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set (Var "a"))  ($#k1_algstr_0 :::"+"::: )  (Set  "("  ($#k4_struct_0 :::"0."::: )  (Set (Var "L")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "a")))  ")" ) & (Bool  "("   "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) (Bool  "ex" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Set (Set (Var "a"))  ($#k1_algstr_0 :::"+"::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set   ($#k4_struct_0 :::"0."::: )  (Set (Var "L")))))  ")" ) & (Bool  "("   "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set  "(" (Set (Var "a"))  ($#k1_algstr_0 :::"+"::: )  (Set (Var "b")) ")" )  ($#k1_algstr_0 :::"+"::: )  (Set (Var "c")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k1_algstr_0 :::"+"::: )  (Set  "(" (Set (Var "b"))  ($#k1_algstr_0 :::"+"::: )  (Set (Var "c")) ")" )))  ")" ) & (Bool  "("   "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set (Var "a"))  ($#k1_algstr_0 :::"+"::: )  (Set (Var "b")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "b"))  ($#k1_algstr_0 :::"+"::: )  (Set (Var "a"))))  ")" ) & (Bool (Set   ($#k4_struct_0 :::"0."::: )  (Set (Var "L")))  ($#r1_hidden :::"<>"::: )  (Set   ($#k5_struct_0 :::"1."::: )  (Set (Var "L")))) & (Bool  "("   "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set (Var "a"))  ($#k6_algstr_0 :::"*"::: )  (Set  "("  ($#k5_struct_0 :::"1."::: )  (Set (Var "L")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "a")))  ")" ) & (Bool  "("   "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L"))  "st" (Bool (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k4_struct_0 :::"0."::: )  (Set (Var "L"))))) "holds"  (Bool  "ex" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Set (Set (Var "a"))  ($#k6_algstr_0 :::"*"::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set   ($#k5_struct_0 :::"1."::: )  (Set (Var "L")))))  ")" ) & (Bool  "("   "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set (Var "a"))  ($#k6_algstr_0 :::"*"::: )  (Set  "("  ($#k4_struct_0 :::"0."::: )  (Set (Var "L")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k4_struct_0 :::"0."::: )  (Set (Var "L"))))  ")" ) & (Bool  "("   "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set  "(" (Set (Var "a"))  ($#k6_algstr_0 :::"*"::: )  (Set (Var "b")) ")" )  ($#k6_algstr_0 :::"*"::: )  (Set (Var "c")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k6_algstr_0 :::"*"::: )  (Set  "(" (Set (Var "b"))  ($#k6_algstr_0 :::"*"::: )  (Set (Var "c")) ")" )))  ")" ) & (Bool  "("   "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set (Var "a"))  ($#k6_algstr_0 :::"*"::: )  (Set  "(" (Set (Var "b"))  ($#k1_algstr_0 :::"+"::: )  (Set (Var "c")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "a"))  ($#k6_algstr_0 :::"*"::: )  (Set (Var "b")) ")" )  ($#k1_algstr_0 :::"+"::: )  (Set  "(" (Set (Var "a"))  ($#k6_algstr_0 :::"*"::: )  (Set (Var "c")) ")" )))  ")" ) & (Bool  "("   "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set (Var "a"))  ($#k6_algstr_0 :::"*"::: )  (Set (Var "b")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "b"))  ($#k6_algstr_0 :::"*"::: )  (Set (Var "a"))))  ")" )  ")" )  ")" )) ;