:: BCIALG_4  semantic presentation begin  definitionattr "c1" is  :::"strict"::: ; struct  :::"BCIStr_1":::  ->    ($#l2_bcialg_1 :::"BCIStr_0"::: )   ","    ($#l2_struct_0 :::"ZeroStr"::: )  ; aggr :::"BCIStr_1":::(# :::"carrier":::, :::"ExternalDiff":::, :::"InternalDiff":::, :::"ZeroF"::: #) ->    ($#l1_bcialg_4 :::"BCIStr_1"::: )  ; sel  :::"ExternalDiff"::: "c1" ->   ($#m1_subset_1 :::"BinOp":::) "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "c1"); end; registration
cluster  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_bcialg_4 :::"strict"::: )    for    ($#l1_bcialg_4 :::"BCIStr_1"::: )  ; 
end; definitionlet "A" be    ($#l1_bcialg_4 :::"BCIStr_1"::: )  ; let "x", "y" be   ($#m1_subset_1 :::"Element":::) "of" (Set (Const "A")); func "x" :::"*"::: "y" ->   ($#m1_subset_1 :::"Element":::) "of" "A" equals :: BCIALG_4:def 1 (Set (Set  "the"  ($#u1_bcialg_4 :::"ExternalDiff"::: )  "of" "A")  ($#k5_binop_1 :::"."::: )   "(" "x" "," "y" ")" ); end; 







:: deftheorem    defines :::"*"::: BCIALG_4:def 1 :  (Bool  "for" (Set (Var "A")) "being"    ($#l1_bcialg_4 :::"BCIStr_1"::: )    (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "A")) "holds"  (Bool (Set (Set (Var "x"))  ($#k1_bcialg_4 :::"*"::: )  (Set (Var "y")))  ($#r1_hidden :::"="::: )  (Set (Set  "the"  ($#u1_bcialg_4 :::"ExternalDiff"::: )  "of" (Set (Var "A")))  ($#k5_binop_1 :::"."::: )   "(" (Set (Var "x")) "," (Set (Var "y")) ")" )))); 
 definitionlet "IT" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_bcialg_4 :::"BCIStr_1"::: )  ; attr "IT" is  :::"with_condition_S":::  means :: BCIALG_4:def 2 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being"   ($#m1_subset_1 :::"Element":::) "of" "IT" "holds"  (Bool (Set (Set  "(" (Set (Var "x"))  ($#k1_bcialg_1 :::"\"::: )  (Set (Var "y")) ")" )  ($#k1_bcialg_1 :::"\"::: )  (Set (Var "z")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "x"))  ($#k1_bcialg_1 :::"\"::: )  (Set  "(" (Set (Var "y"))  ($#k1_bcialg_4 :::"*"::: )  (Set (Var "z")) ")" )))); end; 




:: deftheorem    defines :::"with_condition_S"::: BCIALG_4:def 2 :  (Bool  "for" (Set (Var "IT")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_bcialg_4 :::"BCIStr_1"::: )   "holds"   (Bool  "("  (Bool (Set (Var "IT")) "is"   ($#v2_bcialg_4 :::"with_condition_S"::: )  ) "iff" (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT")) "holds"  (Bool (Set (Set  "(" (Set (Var "x"))  ($#k1_bcialg_1 :::"\"::: )  (Set (Var "y")) ")" )  ($#k1_bcialg_1 :::"\"::: )  (Set (Var "z")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "x"))  ($#k1_bcialg_1 :::"\"::: )  (Set  "(" (Set (Var "y"))  ($#k1_bcialg_4 :::"*"::: )  (Set (Var "z")) ")" ))))  ")" )); 
 definitionfunc  :::"BCI_S-EXAMPLE":::  ->    ($#l1_bcialg_4 :::"BCIStr_1"::: )   equals :: BCIALG_4:def 3 (Set   ($#g1_bcialg_4 :::"BCIStr_1"::: )  "(#"  (Num 1) "," (Set  ($#k9_funct_5 :::"op2"::: ) ) "," (Set  ($#k9_funct_5 :::"op2"::: ) ) "," (Set  ($#k5_funct_5 :::"op0"::: ) ) "#)" ); end; 




:: deftheorem    defines :::"BCI_S-EXAMPLE"::: BCIALG_4:def 3 :  (Bool (Set   ($#k2_bcialg_4 :::"BCI_S-EXAMPLE"::: )  )  ($#r1_hidden :::"="::: )  (Set   ($#g1_bcialg_4 :::"BCIStr_1"::: )  "(#"  (Num 1) "," (Set  ($#k9_funct_5 :::"op2"::: ) ) "," (Set  ($#k9_funct_5 :::"op2"::: ) ) "," (Set  ($#k5_funct_5 :::"op0"::: ) ) "#)" )); 
 registration
cluster (Set   ($#k2_bcialg_4 :::"BCI_S-EXAMPLE"::: )  ) -> (Num 1)  ($#v13_struct_0 :::"-element"::: )     ($#v1_bcialg_4 :::"strict"::: )   ; 
end; registration
cluster (Set   ($#k2_bcialg_4 :::"BCI_S-EXAMPLE"::: )  ) ->   ($#v3_bcialg_1 :::"being_B"::: )     ($#v4_bcialg_1 :::"being_C"::: )     ($#v5_bcialg_1 :::"being_I"::: )     ($#v7_bcialg_1 :::"being_BCI-4"::: )     ($#v8_bcialg_1 :::"being_BCK-5"::: )     ($#v2_bcialg_4 :::"with_condition_S"::: )   ; 
end; registration
cluster  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v3_bcialg_1 :::"being_B"::: )     ($#v4_bcialg_1 :::"being_C"::: )     ($#v5_bcialg_1 :::"being_I"::: )     ($#v7_bcialg_1 :::"being_BCI-4"::: )     ($#v1_bcialg_4 :::"strict"::: )     ($#v2_bcialg_4 :::"with_condition_S"::: )    for    ($#l1_bcialg_4 :::"BCIStr_1"::: )  ; 
end; definitionmode BCI-Algebra_with_Condition(S) is  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v3_bcialg_1 :::"being_B"::: )     ($#v4_bcialg_1 :::"being_C"::: )     ($#v5_bcialg_1 :::"being_I"::: )     ($#v7_bcialg_1 :::"being_BCI-4"::: )     ($#v2_bcialg_4 :::"with_condition_S"::: )     ($#l1_bcialg_4 :::"BCIStr_1"::: )  ; end; 













definitionlet "X" be   ($#l1_bcialg_4 :::"BCI-Algebra_with_Condition(S)":::); let "x", "y" be   ($#m1_subset_1 :::"Element":::) "of" (Set (Const "X")); func  :::"Condition_S":::  "(" "x" "," "y" ")"  ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_subset_1 :::"Subset":::) "of" "X" equals :: BCIALG_4:def 4  "{"  (Set (Var "t")) where t "is"   ($#m1_subset_1 :::"Element":::) "of" "X" : (Bool (Set (Set (Var "t"))  ($#k1_bcialg_1 :::"\"::: )  "x")  ($#r1_bcialg_1 :::"<="::: )  "y")  "}"  ; end; 







:: deftheorem    defines :::"Condition_S"::: BCIALG_4:def 4 :  (Bool  "for" (Set (Var "X")) "being"   ($#l1_bcialg_4 :::"BCI-Algebra_with_Condition(S)":::)  (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "holds"  (Bool (Set   ($#k3_bcialg_4 :::"Condition_S"::: )   "(" (Set (Var "x")) "," (Set (Var "y")) ")" )  ($#r1_hidden :::"="::: )   "{"  (Set (Var "t")) where t "is"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) : (Bool (Set (Set (Var "t"))  ($#k1_bcialg_1 :::"\"::: )  (Set (Var "x")))  ($#r1_bcialg_1 :::"<="::: )  (Set (Var "y")))  "}"  ))); 
 
theorem :: BCIALG_4:1 (Bool  "for" (Set (Var "X")) "being"   ($#l1_bcialg_4 :::"BCI-Algebra_with_Condition(S)":::)  (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "u")) "," (Set (Var "v")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X"))  "st" (Bool (Bool (Set (Var "u"))  ($#r2_hidden :::"in"::: )  (Set   ($#k3_bcialg_4 :::"Condition_S"::: )   "(" (Set (Var "x")) "," (Set (Var "y")) ")" )) & (Bool (Set (Var "v"))  ($#r1_bcialg_1 :::"<="::: )  (Set (Var "u")))) "holds"  (Bool (Set (Var "v"))  ($#r2_hidden :::"in"::: )  (Set   ($#k3_bcialg_4 :::"Condition_S"::: )   "(" (Set (Var "x")) "," (Set (Var "y")) ")" )))) ; 
 
theorem :: BCIALG_4:2 (Bool  "for" (Set (Var "X")) "being"   ($#l1_bcialg_4 :::"BCI-Algebra_with_Condition(S)":::)  (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) (Bool  "ex" (Set (Var "a")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k3_bcialg_4 :::"Condition_S"::: )   "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) "st"  (Bool  "for" (Set (Var "z")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k3_bcialg_4 :::"Condition_S"::: )   "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) "holds"  (Bool (Set (Var "z"))  ($#r1_bcialg_1 :::"<="::: )  (Set (Var "a"))))))) ; 
 
theorem :: BCIALG_4:3 (Bool  "for" (Set (Var "X")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_bcialg_4 :::"BCIStr_1"::: )   "holds"   (Bool  "("  (Bool  "("  (Bool (Set (Var "X")) "is"   ($#l2_bcialg_1 :::"BCI-algebra":::)) & (Bool  "("   "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "holds"   (Bool  "("  (Bool (Set (Set  "(" (Set (Var "x"))  ($#k1_bcialg_4 :::"*"::: )  (Set (Var "y")) ")" )  ($#k1_bcialg_1 :::"\"::: )  (Set (Var "x")))  ($#r1_bcialg_1 :::"<="::: )  (Set (Var "y"))) & (Bool  "("   "for" (Set (Var "t")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X"))  "st" (Bool (Bool (Set (Set (Var "t"))  ($#k1_bcialg_1 :::"\"::: )  (Set (Var "x")))  ($#r1_bcialg_1 :::"<="::: )  (Set (Var "y")))) "holds"  (Bool (Set (Var "t"))  ($#r1_bcialg_1 :::"<="::: )  (Set (Set (Var "x"))  ($#k1_bcialg_4 :::"*"::: )  (Set (Var "y"))))  ")" )  ")" )  ")" )  ")" ) "iff" (Bool (Set (Var "X")) "is"   ($#l1_bcialg_4 :::"BCI-Algebra_with_Condition(S)":::))  ")" )) ; 
 
theorem :: BCIALG_4:4 (Bool  "for" (Set (Var "X")) "being"   ($#l1_bcialg_4 :::"BCI-Algebra_with_Condition(S)":::)  (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) (Bool  "ex" (Set (Var "a")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k3_bcialg_4 :::"Condition_S"::: )   "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) "st"  (Bool  "for" (Set (Var "z")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k3_bcialg_4 :::"Condition_S"::: )   "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) "holds"  (Bool (Set (Var "z"))  ($#r1_bcialg_1 :::"<="::: )  (Set (Var "a"))))))) ; 
 definitionlet "X" be   ($#v19_bcialg_1 :::"p-Semisimple"::: )    ($#l2_bcialg_1 :::"BCI-algebra":::); func  :::"Adjoint_pGroup"::: "X" ->   ($#v8_algstr_0 :::"strict"::: )    ($#l2_algstr_0 :::"AbGroup":::) means :: BCIALG_4:def 5 (Bool  "("  (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" it)  ($#r1_hidden :::"="::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "X")) & (Bool  "("   "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Element":::) "of" "X" "holds"  (Bool (Set (Set  "the"  ($#u1_algstr_0 :::"addF"::: )  "of" it)  ($#k1_binop_1 :::"."::: )   "(" (Set (Var "x")) "," (Set (Var "y")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set (Var "x"))  ($#k1_bcialg_1 :::"\"::: )  (Set  "(" (Set  "("  ($#k4_struct_0 :::"0."::: )  "X" ")" )  ($#k1_bcialg_1 :::"\"::: )  (Set (Var "y")) ")" )))  ")" ) & (Bool (Set   ($#k4_struct_0 :::"0."::: )  it)  ($#r1_hidden :::"="::: )  (Set   ($#k4_struct_0 :::"0."::: )  "X"))  ")" ); end; 





:: deftheorem    defines :::"Adjoint_pGroup"::: BCIALG_4:def 5 :  (Bool  "for" (Set (Var "X")) "being"   ($#v19_bcialg_1 :::"p-Semisimple"::: )    ($#l2_bcialg_1 :::"BCI-algebra":::)  (Bool  "for" (Set (Var "b2")) "being"   ($#v8_algstr_0 :::"strict"::: )    ($#l2_algstr_0 :::"AbGroup":::) "holds"   (Bool  "("  (Bool (Set (Var "b2"))  ($#r1_hidden :::"="::: )  (Set   ($#k4_bcialg_4 :::"Adjoint_pGroup"::: )  (Set (Var "X")))) "iff" (Bool  "("  (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "b2")))  ($#r1_hidden :::"="::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "X")))) & (Bool  "("   "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "holds"  (Bool (Set (Set  "the"  ($#u1_algstr_0 :::"addF"::: )  "of" (Set (Var "b2")))  ($#k1_binop_1 :::"."::: )   "(" (Set (Var "x")) "," (Set (Var "y")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set (Var "x"))  ($#k1_bcialg_1 :::"\"::: )  (Set  "(" (Set  "("  ($#k4_struct_0 :::"0."::: )  (Set (Var "X")) ")" )  ($#k1_bcialg_1 :::"\"::: )  (Set (Var "y")) ")" )))  ")" ) & (Bool (Set   ($#k4_struct_0 :::"0."::: )  (Set (Var "b2")))  ($#r1_hidden :::"="::: )  (Set   ($#k4_struct_0 :::"0."::: )  (Set (Var "X"))))  ")" )  ")" ))); 
 
theorem :: BCIALG_4:5 (Bool  "for" (Set (Var "X")) "being"   ($#l2_bcialg_1 :::"BCI-algebra":::) "holds"   (Bool  "("  (Bool (Set (Var "X")) "is"   ($#v19_bcialg_1 :::"p-Semisimple"::: )  ) "iff" (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X"))  "st" (Bool (Bool (Set (Set (Var "x"))  ($#k1_bcialg_1 :::"\"::: )  (Set (Var "y")))  ($#r1_hidden :::"="::: )  (Set   ($#k4_struct_0 :::"0."::: )  (Set (Var "X"))))) "holds"  (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set (Var "y"))))  ")" )) ; 
 
theorem :: BCIALG_4:6 (Bool  "for" (Set (Var "X")) "being"   ($#l1_bcialg_4 :::"BCI-Algebra_with_Condition(S)":::)  "st" (Bool (Bool (Set (Var "X")) "is"   ($#v19_bcialg_1 :::"p-Semisimple"::: )  )) "holds"  (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "holds"  (Bool (Set (Set (Var "x"))  ($#k1_bcialg_4 :::"*"::: )  (Set (Var "y")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "x"))  ($#k1_bcialg_1 :::"\"::: )  (Set  "(" (Set  "("  ($#k4_struct_0 :::"0."::: )  (Set (Var "X")) ")" )  ($#k1_bcialg_1 :::"\"::: )  (Set (Var "y")) ")" ))))) ; 
 
theorem :: BCIALG_4:7 (Bool  "for" (Set (Var "X")) "being"   ($#l1_bcialg_4 :::"BCI-Algebra_with_Condition(S)":::)  (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "holds"  (Bool (Set (Set (Var "x"))  ($#k1_bcialg_4 :::"*"::: )  (Set (Var "y")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "y"))  ($#k1_bcialg_4 :::"*"::: )  (Set (Var "x")))))) ; 
 
theorem :: BCIALG_4:8 (Bool  "for" (Set (Var "X")) "being"   ($#l1_bcialg_4 :::"BCI-Algebra_with_Condition(S)":::)  (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X"))  "st" (Bool (Bool (Set (Var "x"))  ($#r1_bcialg_1 :::"<="::: )  (Set (Var "y")))) "holds"  (Bool  "("  (Bool (Set (Set (Var "x"))  ($#k1_bcialg_4 :::"*"::: )  (Set (Var "z")))  ($#r1_bcialg_1 :::"<="::: )  (Set (Set (Var "y"))  ($#k1_bcialg_4 :::"*"::: )  (Set (Var "z")))) & (Bool (Set (Set (Var "z"))  ($#k1_bcialg_4 :::"*"::: )  (Set (Var "x")))  ($#r1_bcialg_1 :::"<="::: )  (Set (Set (Var "z"))  ($#k1_bcialg_4 :::"*"::: )  (Set (Var "y"))))  ")" ))) ; 
 
theorem :: BCIALG_4:9 (Bool  "for" (Set (Var "X")) "being"   ($#l1_bcialg_4 :::"BCI-Algebra_with_Condition(S)":::)  (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "holds"   (Bool  "("  (Bool (Set (Set  "("  ($#k4_struct_0 :::"0."::: )  (Set (Var "X")) ")" )  ($#k1_bcialg_4 :::"*"::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Var "x"))) & (Bool (Set (Set (Var "x"))  ($#k1_bcialg_4 :::"*"::: )  (Set  "("  ($#k4_struct_0 :::"0."::: )  (Set (Var "X")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "x")))  ")" ))) ; 
 
theorem :: BCIALG_4:10 (Bool  "for" (Set (Var "X")) "being"   ($#l1_bcialg_4 :::"BCI-Algebra_with_Condition(S)":::)  (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "holds"  (Bool (Set (Set  "(" (Set (Var "x"))  ($#k1_bcialg_4 :::"*"::: )  (Set (Var "y")) ")" )  ($#k1_bcialg_4 :::"*"::: )  (Set (Var "z")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "x"))  ($#k1_bcialg_4 :::"*"::: )  (Set  "(" (Set (Var "y"))  ($#k1_bcialg_4 :::"*"::: )  (Set (Var "z")) ")" ))))) ; 
 
theorem :: BCIALG_4:11 (Bool  "for" (Set (Var "X")) "being"   ($#l1_bcialg_4 :::"BCI-Algebra_with_Condition(S)":::)  (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "holds"  (Bool (Set (Set  "(" (Set (Var "x"))  ($#k1_bcialg_4 :::"*"::: )  (Set (Var "y")) ")" )  ($#k1_bcialg_4 :::"*"::: )  (Set (Var "z")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "x"))  ($#k1_bcialg_4 :::"*"::: )  (Set (Var "z")) ")" )  ($#k1_bcialg_4 :::"*"::: )  (Set (Var "y")))))) ; 
 
theorem :: BCIALG_4:12 (Bool  "for" (Set (Var "X")) "being"   ($#l1_bcialg_4 :::"BCI-Algebra_with_Condition(S)":::)  (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "holds"  (Bool (Set (Set  "(" (Set (Var "x"))  ($#k1_bcialg_1 :::"\"::: )  (Set (Var "y")) ")" )  ($#k1_bcialg_1 :::"\"::: )  (Set (Var "z")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "x"))  ($#k1_bcialg_1 :::"\"::: )  (Set  "(" (Set (Var "y"))  ($#k1_bcialg_4 :::"*"::: )  (Set (Var "z")) ")" ))))) ; 
 
theorem :: BCIALG_4:13 (Bool  "for" (Set (Var "X")) "being"   ($#l1_bcialg_4 :::"BCI-Algebra_with_Condition(S)":::)  (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "holds"  (Bool (Set (Var "y"))  ($#r1_bcialg_1 :::"<="::: )  (Set (Set (Var "x"))  ($#k1_bcialg_4 :::"*"::: )  (Set  "(" (Set (Var "y"))  ($#k1_bcialg_1 :::"\"::: )  (Set (Var "x")) ")" ))))) ; 
 
theorem :: BCIALG_4:14 (Bool  "for" (Set (Var "X")) "being"   ($#l1_bcialg_4 :::"BCI-Algebra_with_Condition(S)":::)  (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "holds"  (Bool (Set (Set  "(" (Set (Var "x"))  ($#k1_bcialg_4 :::"*"::: )  (Set (Var "z")) ")" )  ($#k1_bcialg_1 :::"\"::: )  (Set  "(" (Set (Var "y"))  ($#k1_bcialg_4 :::"*"::: )  (Set (Var "z")) ")" ))  ($#r1_bcialg_1 :::"<="::: )  (Set (Set (Var "x"))  ($#k1_bcialg_1 :::"\"::: )  (Set (Var "y")))))) ; 
 
theorem :: BCIALG_4:15 (Bool  "for" (Set (Var "X")) "being"   ($#l1_bcialg_4 :::"BCI-Algebra_with_Condition(S)":::)  (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "holds"   (Bool  "("  (Bool (Set (Set (Var "x"))  ($#k1_bcialg_1 :::"\"::: )  (Set (Var "y")))  ($#r1_bcialg_1 :::"<="::: )  (Set (Var "z"))) "iff" (Bool (Set (Var "x"))  ($#r1_bcialg_1 :::"<="::: )  (Set (Set (Var "y"))  ($#k1_bcialg_4 :::"*"::: )  (Set (Var "z"))))  ")" ))) ; 
 
theorem :: BCIALG_4:16 (Bool  "for" (Set (Var "X")) "being"   ($#l1_bcialg_4 :::"BCI-Algebra_with_Condition(S)":::)  (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "holds"  (Bool (Set (Set (Var "x"))  ($#k1_bcialg_1 :::"\"::: )  (Set (Var "y")))  ($#r1_bcialg_1 :::"<="::: )  (Set (Set  "(" (Set (Var "x"))  ($#k1_bcialg_1 :::"\"::: )  (Set (Var "z")) ")" )  ($#k1_bcialg_4 :::"*"::: )  (Set  "(" (Set (Var "z"))  ($#k1_bcialg_1 :::"\"::: )  (Set (Var "y")) ")" ))))) ; 
 registrationlet "X" be   ($#l1_bcialg_4 :::"BCI-Algebra_with_Condition(S)":::); 
cluster (Set  "the"  ($#u1_bcialg_4 :::"ExternalDiff"::: )  "of" "X") ->   ($#v1_binop_1 :::"commutative"::: )     ($#v2_binop_1 :::"associative"::: )   ; 
end; 
theorem :: BCIALG_4:17 (Bool  "for" (Set (Var "X")) "being"   ($#l1_bcialg_4 :::"BCI-Algebra_with_Condition(S)":::) "holds"  (Bool (Set   ($#k4_struct_0 :::"0."::: )  (Set (Var "X")))  ($#r3_binop_1 :::"is_a_unity_wrt"::: )  (Set  "the"  ($#u1_bcialg_4 :::"ExternalDiff"::: )  "of" (Set (Var "X"))))) ; 
 
theorem :: BCIALG_4:18 (Bool  "for" (Set (Var "X")) "being"   ($#l1_bcialg_4 :::"BCI-Algebra_with_Condition(S)":::) "holds"  (Bool (Set   ($#k4_binop_1 :::"the_unity_wrt"::: )  (Set  "the"  ($#u1_bcialg_4 :::"ExternalDiff"::: )  "of" (Set (Var "X"))))  ($#r1_hidden :::"="::: )  (Set   ($#k4_struct_0 :::"0."::: )  (Set (Var "X"))))) ; 
 
theorem :: BCIALG_4:19 (Bool  "for" (Set (Var "X")) "being"   ($#l1_bcialg_4 :::"BCI-Algebra_with_Condition(S)":::) "holds"  (Bool (Set  "the"  ($#u1_bcialg_4 :::"ExternalDiff"::: )  "of" (Set (Var "X"))) "is"   ($#v1_setwiseo :::"having_a_unity"::: )  )) ; 
 definitionlet "X" be   ($#l1_bcialg_4 :::"BCI-Algebra_with_Condition(S)":::); func  :::"power"::: "X" ->   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "X") "," (Set  ($#k5_numbers :::"NAT"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "X") means :: BCIALG_4:def 6 (Bool  "for" (Set (Var "h")) "being"   ($#m1_subset_1 :::"Element":::) "of" "X" "holds"   (Bool  "("  (Bool (Set it  ($#k2_binop_1 :::"."::: )   "(" (Set (Var "h")) "," (Set  ($#k6_numbers :::"0"::: ) ) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k4_struct_0 :::"0."::: )  "X")) & (Bool  "("   "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set it  ($#k2_binop_1 :::"."::: )   "(" (Set (Var "h")) "," (Set  "(" (Set (Var "n"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "(" it  ($#k2_binop_1 :::"."::: )   "(" (Set (Var "h")) "," (Set (Var "n")) ")"  ")" )  ($#k1_bcialg_4 :::"*"::: )  (Set (Var "h"))))  ")" )  ")" )); end; 





:: deftheorem    defines :::"power"::: BCIALG_4:def 6 :  (Bool  "for" (Set (Var "X")) "being"   ($#l1_bcialg_4 :::"BCI-Algebra_with_Condition(S)":::)  (Bool  "for" (Set (Var "b2")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "X"))) "," (Set  ($#k5_numbers :::"NAT"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "X"))) "holds"   (Bool  "("  (Bool (Set (Var "b2"))  ($#r1_hidden :::"="::: )  (Set   ($#k5_bcialg_4 :::"power"::: )  (Set (Var "X")))) "iff" (Bool  "for" (Set (Var "h")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "holds"   (Bool  "("  (Bool (Set (Set (Var "b2"))  ($#k2_binop_1 :::"."::: )   "(" (Set (Var "h")) "," (Set  ($#k6_numbers :::"0"::: ) ) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k4_struct_0 :::"0."::: )  (Set (Var "X")))) & (Bool  "("   "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set (Set (Var "b2"))  ($#k2_binop_1 :::"."::: )   "(" (Set (Var "h")) "," (Set  "(" (Set (Var "n"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "b2"))  ($#k2_binop_1 :::"."::: )   "(" (Set (Var "h")) "," (Set (Var "n")) ")"  ")" )  ($#k1_bcialg_4 :::"*"::: )  (Set (Var "h"))))  ")" )  ")" ))  ")" ))); 
 definitionlet "X" be   ($#l1_bcialg_4 :::"BCI-Algebra_with_Condition(S)":::); let "x" be   ($#m1_subset_1 :::"Element":::) "of" (Set (Const "X")); let "n" be    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ); func "x" :::"|^"::: "n" ->   ($#m1_subset_1 :::"Element":::) "of" "X" equals :: BCIALG_4:def 7 (Set (Set  "("  ($#k5_bcialg_4 :::"power"::: )  "X" ")" )  ($#k2_binop_1 :::"."::: )   "(" "x" "," "n" ")" ); end; 







:: deftheorem    defines :::"|^"::: BCIALG_4:def 7 :  (Bool  "for" (Set (Var "X")) "being"   ($#l1_bcialg_4 :::"BCI-Algebra_with_Condition(S)":::)  (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X"))  (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set (Set (Var "x"))  ($#k6_bcialg_4 :::"|^"::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k5_bcialg_4 :::"power"::: )  (Set (Var "X")) ")" )  ($#k2_binop_1 :::"."::: )   "(" (Set (Var "x")) "," (Set (Var "n")) ")" ))))); 
 
theorem :: BCIALG_4:20 (Bool  "for" (Set (Var "X")) "being"   ($#l1_bcialg_4 :::"BCI-Algebra_with_Condition(S)":::)  (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "holds"  (Bool (Set (Set (Var "x"))  ($#k6_bcialg_4 :::"|^"::: )  (Set  ($#k6_numbers :::"0"::: ) ))  ($#r1_hidden :::"="::: )  (Set   ($#k4_struct_0 :::"0."::: )  (Set (Var "X")))))) ; 
 
theorem :: BCIALG_4:21 (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "X")) "being"   ($#l1_bcialg_4 :::"BCI-Algebra_with_Condition(S)":::)  (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "holds"  (Bool (Set (Set (Var "x"))  ($#k6_bcialg_4 :::"|^"::: )  (Set  "(" (Set (Var "n"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "x"))  ($#k6_bcialg_4 :::"|^"::: )  (Set (Var "n")) ")" )  ($#k1_bcialg_4 :::"*"::: )  (Set (Var "x"))))))) ; 
 
theorem :: BCIALG_4:22 (Bool  "for" (Set (Var "X")) "being"   ($#l1_bcialg_4 :::"BCI-Algebra_with_Condition(S)":::)  (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "holds"  (Bool (Set (Set (Var "x"))  ($#k6_bcialg_4 :::"|^"::: )  (Num 1))  ($#r1_hidden :::"="::: )  (Set (Var "x"))))) ; 
 
theorem :: BCIALG_4:23 (Bool  "for" (Set (Var "X")) "being"   ($#l1_bcialg_4 :::"BCI-Algebra_with_Condition(S)":::)  (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "holds"  (Bool (Set (Set (Var "x"))  ($#k6_bcialg_4 :::"|^"::: )  (Num 2))  ($#r1_hidden :::"="::: )  (Set (Set (Var "x"))  ($#k1_bcialg_4 :::"*"::: )  (Set (Var "x")))))) ; 
 
theorem :: BCIALG_4:24 (Bool  "for" (Set (Var "X")) "being"   ($#l1_bcialg_4 :::"BCI-Algebra_with_Condition(S)":::)  (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "holds"  (Bool (Set (Set (Var "x"))  ($#k6_bcialg_4 :::"|^"::: )  (Num 3))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "x"))  ($#k1_bcialg_4 :::"*"::: )  (Set (Var "x")) ")" )  ($#k1_bcialg_4 :::"*"::: )  (Set (Var "x")))))) ; 
 
theorem :: BCIALG_4:25 (Bool  "for" (Set (Var "X")) "being"   ($#l1_bcialg_4 :::"BCI-Algebra_with_Condition(S)":::) "holds"  (Bool (Set (Set  "("  ($#k4_struct_0 :::"0."::: )  (Set (Var "X")) ")" )  ($#k6_bcialg_4 :::"|^"::: )  (Num 2))  ($#r1_hidden :::"="::: )  (Set   ($#k4_struct_0 :::"0."::: )  (Set (Var "X"))))) ; 
 
theorem :: BCIALG_4:26 (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "X")) "being"   ($#l1_bcialg_4 :::"BCI-Algebra_with_Condition(S)":::) "holds"  (Bool (Set (Set  "("  ($#k4_struct_0 :::"0."::: )  (Set (Var "X")) ")" )  ($#k6_bcialg_4 :::"|^"::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set   ($#k4_struct_0 :::"0."::: )  (Set (Var "X")))))) ; 
 
theorem :: BCIALG_4:27 (Bool  "for" (Set (Var "X")) "being"   ($#l1_bcialg_4 :::"BCI-Algebra_with_Condition(S)":::)  (Bool  "for" (Set (Var "x")) "," (Set (Var "a")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "holds"  (Bool (Set (Set  "(" (Set  "(" (Set (Var "x"))  ($#k1_bcialg_1 :::"\"::: )  (Set (Var "a")) ")" )  ($#k1_bcialg_1 :::"\"::: )  (Set (Var "a")) ")" )  ($#k1_bcialg_1 :::"\"::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "x"))  ($#k1_bcialg_1 :::"\"::: )  (Set  "(" (Set (Var "a"))  ($#k6_bcialg_4 :::"|^"::: )  (Num 3) ")" ))))) ; 
 
theorem :: BCIALG_4:28 (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "X")) "being"   ($#l1_bcialg_4 :::"BCI-Algebra_with_Condition(S)":::)  (Bool  "for" (Set (Var "x")) "," (Set (Var "a")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "holds"  (Bool (Set  "(" (Set (Var "x")) "," (Set (Var "a")) ")"   ($#k1_bcialg_2 :::"to_power"::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "x"))  ($#k1_bcialg_1 :::"\"::: )  (Set  "(" (Set (Var "a"))  ($#k6_bcialg_4 :::"|^"::: )  (Set (Var "n")) ")" )))))) ; 
 definitionlet "X" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_bcialg_4 :::"BCIStr_1"::: )  ; let "F" be    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Const "X"))); func  :::"Product_S"::: "F" ->   ($#m1_subset_1 :::"Element":::) "of" "X" equals :: BCIALG_4:def 8 (Set (Set  "the"  ($#u1_bcialg_4 :::"ExternalDiff"::: )  "of" "X")  ($#k1_finsop_1 :::""**""::: )  "F"); end; 






:: deftheorem    defines :::"Product_S"::: BCIALG_4:def 8 :  (Bool  "for" (Set (Var "X")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_bcialg_4 :::"BCIStr_1"::: )    (Bool  "for" (Set (Var "F")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "X"))) "holds"  (Bool (Set   ($#k7_bcialg_4 :::"Product_S"::: )  (Set (Var "F")))  ($#r1_hidden :::"="::: )  (Set (Set  "the"  ($#u1_bcialg_4 :::"ExternalDiff"::: )  "of" (Set (Var "X")))  ($#k1_finsop_1 :::""**""::: )  (Set (Var "F")))))); 
 
theorem :: BCIALG_4:29 (Bool  "for" (Set (Var "X")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_bcialg_4 :::"BCIStr_1"::: )    (Bool  "for" (Set (Var "d")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "holds"  (Bool (Set (Set  "the"  ($#u1_bcialg_4 :::"ExternalDiff"::: )  "of" (Set (Var "X")))  ($#k1_finsop_1 :::""**""::: )  (Set  ($#k12_finseq_1 :::"<*"::: ) (Set (Var "d")) ($#k12_finseq_1 :::"*>"::: ) ))  ($#r1_hidden :::"="::: )  (Set (Var "d"))))) ; 
 
theorem :: BCIALG_4:30 (Bool  "for" (Set (Var "X")) "being"   ($#l1_bcialg_4 :::"BCI-Algebra_with_Condition(S)":::)  (Bool  "for" (Set (Var "F1")) "," (Set (Var "F2")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "X"))) "holds"  (Bool (Set   ($#k7_bcialg_4 :::"Product_S"::: )  (Set  "(" (Set (Var "F1"))  ($#k8_finseq_1 :::"^"::: )  (Set (Var "F2")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k7_bcialg_4 :::"Product_S"::: )  (Set (Var "F1")) ")" )  ($#k1_bcialg_4 :::"*"::: )  (Set  "("  ($#k7_bcialg_4 :::"Product_S"::: )  (Set (Var "F2")) ")" ))))) ; 
 
theorem :: BCIALG_4:31 (Bool  "for" (Set (Var "X")) "being"   ($#l1_bcialg_4 :::"BCI-Algebra_with_Condition(S)":::)  (Bool  "for" (Set (Var "F")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "X")))  (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "holds"  (Bool (Set   ($#k7_bcialg_4 :::"Product_S"::: )  (Set  "(" (Set (Var "F"))  ($#k8_finseq_1 :::"^"::: )  (Set  ($#k12_finseq_1 :::"<*"::: ) (Set (Var "a")) ($#k12_finseq_1 :::"*>"::: ) ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k7_bcialg_4 :::"Product_S"::: )  (Set (Var "F")) ")" )  ($#k1_bcialg_4 :::"*"::: )  (Set (Var "a"))))))) ; 
 
theorem :: BCIALG_4:32 (Bool  "for" (Set (Var "X")) "being"   ($#l1_bcialg_4 :::"BCI-Algebra_with_Condition(S)":::)  (Bool  "for" (Set (Var "F")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "X")))  (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "holds"  (Bool (Set   ($#k7_bcialg_4 :::"Product_S"::: )  (Set  "(" (Set  ($#k12_finseq_1 :::"<*"::: ) (Set (Var "a")) ($#k12_finseq_1 :::"*>"::: ) )  ($#k8_finseq_1 :::"^"::: )  (Set (Var "F")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k1_bcialg_4 :::"*"::: )  (Set  "("  ($#k7_bcialg_4 :::"Product_S"::: )  (Set (Var "F")) ")" )))))) ; 
 
theorem :: BCIALG_4:33 (Bool  "for" (Set (Var "X")) "being"   ($#l1_bcialg_4 :::"BCI-Algebra_with_Condition(S)":::)  (Bool  "for" (Set (Var "a1")) "," (Set (Var "a2")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "holds"  (Bool (Set   ($#k7_bcialg_4 :::"Product_S"::: )  (Set  ($#k2_finseq_4 :::"<*"::: ) (Set (Var "a1")) "," (Set (Var "a2")) ($#k2_finseq_4 :::"*>"::: ) ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a1"))  ($#k1_bcialg_4 :::"*"::: )  (Set (Var "a2")))))) ; 
 
theorem :: BCIALG_4:34 (Bool  "for" (Set (Var "X")) "being"   ($#l1_bcialg_4 :::"BCI-Algebra_with_Condition(S)":::)  (Bool  "for" (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "holds"  (Bool (Set   ($#k7_bcialg_4 :::"Product_S"::: )  (Set  ($#k3_finseq_4 :::"<*"::: ) (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) ($#k3_finseq_4 :::"*>"::: ) ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "a1"))  ($#k1_bcialg_4 :::"*"::: )  (Set (Var "a2")) ")" )  ($#k1_bcialg_4 :::"*"::: )  (Set (Var "a3")))))) ; 
 
theorem :: BCIALG_4:35 (Bool  "for" (Set (Var "X")) "being"   ($#l1_bcialg_4 :::"BCI-Algebra_with_Condition(S)":::)  (Bool  "for" (Set (Var "x")) "," (Set (Var "a1")) "," (Set (Var "a2")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "holds"  (Bool (Set (Set  "(" (Set (Var "x"))  ($#k1_bcialg_1 :::"\"::: )  (Set (Var "a1")) ")" )  ($#k1_bcialg_1 :::"\"::: )  (Set (Var "a2")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "x"))  ($#k1_bcialg_1 :::"\"::: )  (Set  "("  ($#k7_bcialg_4 :::"Product_S"::: )  (Set  ($#k2_finseq_4 :::"<*"::: ) (Set (Var "a1")) "," (Set (Var "a2")) ($#k2_finseq_4 :::"*>"::: ) ) ")" ))))) ; 
 
theorem :: BCIALG_4:36 (Bool  "for" (Set (Var "X")) "being"   ($#l1_bcialg_4 :::"BCI-Algebra_with_Condition(S)":::)  (Bool  "for" (Set (Var "x")) "," (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "holds"  (Bool (Set (Set  "(" (Set  "(" (Set (Var "x"))  ($#k1_bcialg_1 :::"\"::: )  (Set (Var "a1")) ")" )  ($#k1_bcialg_1 :::"\"::: )  (Set (Var "a2")) ")" )  ($#k1_bcialg_1 :::"\"::: )  (Set (Var "a3")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "x"))  ($#k1_bcialg_1 :::"\"::: )  (Set  "("  ($#k7_bcialg_4 :::"Product_S"::: )  (Set  ($#k3_finseq_4 :::"<*"::: ) (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) ($#k3_finseq_4 :::"*>"::: ) ) ")" ))))) ; 
 
theorem :: BCIALG_4:37 (Bool  "for" (Set (Var "X")) "being"   ($#l1_bcialg_4 :::"BCI-Algebra_with_Condition(S)":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_bcialg_1 :::"AtomSet"::: )  (Set (Var "X")))  (Bool  "for" (Set (Var "ma")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X"))  "st" (Bool (Bool  "("   "for" (Set (Var "x")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k7_bcialg_1 :::"BranchV"::: )  (Set (Var "a"))) "holds"  (Bool (Set (Var "x"))  ($#r1_bcialg_1 :::"<="::: )  (Set (Var "ma")))  ")" )) "holds"  (Bool  "ex" (Set (Var "mb")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "st"  (Bool  "for" (Set (Var "y")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k7_bcialg_1 :::"BranchV"::: )  (Set (Var "b"))) "holds"  (Bool (Set (Var "y"))  ($#r1_bcialg_1 :::"<="::: )  (Set (Var "mb")))))))) ; 
 registration
cluster  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v3_bcialg_1 :::"being_B"::: )     ($#v4_bcialg_1 :::"being_C"::: )     ($#v5_bcialg_1 :::"being_I"::: )     ($#v7_bcialg_1 :::"being_BCI-4"::: )     ($#v8_bcialg_1 :::"being_BCK-5"::: )     ($#v1_bcialg_4 :::"strict"::: )     ($#v2_bcialg_4 :::"with_condition_S"::: )    for    ($#l1_bcialg_4 :::"BCIStr_1"::: )  ; 
end; definitionmode BCK-Algebra_with_Condition(S) is   ($#v8_bcialg_1 :::"being_BCK-5"::: )    ($#l1_bcialg_4 :::"BCI-Algebra_with_Condition(S)":::); end; 
theorem :: BCIALG_4:38 (Bool  "for" (Set (Var "X")) "being"   ($#l1_bcialg_4 :::"BCK-Algebra_with_Condition(S)":::)  (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "holds"   (Bool  "("  (Bool (Set (Var "x"))  ($#r1_bcialg_1 :::"<="::: )  (Set (Set (Var "x"))  ($#k1_bcialg_4 :::"*"::: )  (Set (Var "y")))) & (Bool (Set (Var "y"))  ($#r1_bcialg_1 :::"<="::: )  (Set (Set (Var "x"))  ($#k1_bcialg_4 :::"*"::: )  (Set (Var "y"))))  ")" ))) ; 
 
theorem :: BCIALG_4:39 (Bool  "for" (Set (Var "X")) "being"   ($#l1_bcialg_4 :::"BCK-Algebra_with_Condition(S)":::)  (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "holds"  (Bool (Set (Set  "(" (Set  "(" (Set (Var "x"))  ($#k1_bcialg_4 :::"*"::: )  (Set (Var "y")) ")" )  ($#k1_bcialg_1 :::"\"::: )  (Set  "(" (Set (Var "y"))  ($#k1_bcialg_4 :::"*"::: )  (Set (Var "z")) ")" ) ")" )  ($#k1_bcialg_1 :::"\"::: )  (Set  "(" (Set (Var "z"))  ($#k1_bcialg_4 :::"*"::: )  (Set (Var "x")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k4_struct_0 :::"0."::: )  (Set (Var "X")))))) ; 
 
theorem :: BCIALG_4:40 (Bool  "for" (Set (Var "X")) "being"   ($#l1_bcialg_4 :::"BCK-Algebra_with_Condition(S)":::)  (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "holds"  (Bool (Set (Set  "(" (Set (Var "x"))  ($#k1_bcialg_1 :::"\"::: )  (Set (Var "y")) ")" )  ($#k1_bcialg_4 :::"*"::: )  (Set  "(" (Set (Var "y"))  ($#k1_bcialg_1 :::"\"::: )  (Set (Var "x")) ")" ))  ($#r1_bcialg_1 :::"<="::: )  (Set (Set (Var "x"))  ($#k1_bcialg_4 :::"*"::: )  (Set (Var "y")))))) ; 
 
theorem :: BCIALG_4:41 (Bool  "for" (Set (Var "X")) "being"   ($#l1_bcialg_4 :::"BCK-Algebra_with_Condition(S)":::)  (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "holds"  (Bool (Set (Set  "(" (Set (Var "x"))  ($#k1_bcialg_1 :::"\"::: )  (Set  "("  ($#k4_struct_0 :::"0."::: )  (Set (Var "X")) ")" ) ")" )  ($#k1_bcialg_4 :::"*"::: )  (Set  "(" (Set  "("  ($#k4_struct_0 :::"0."::: )  (Set (Var "X")) ")" )  ($#k1_bcialg_1 :::"\"::: )  (Set (Var "x")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "x"))))) ; 
 definitionlet "IT" be   ($#l1_bcialg_4 :::"BCK-Algebra_with_Condition(S)":::); attr "IT" is  :::"commutative":::  means :: BCIALG_4:def 9 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Element":::) "of" "IT" "holds"  (Bool (Set (Set (Var "x"))  ($#k1_bcialg_1 :::"\"::: )  (Set  "(" (Set (Var "x"))  ($#k1_bcialg_1 :::"\"::: )  (Set (Var "y")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "y"))  ($#k1_bcialg_1 :::"\"::: )  (Set  "(" (Set (Var "y"))  ($#k1_bcialg_1 :::"\"::: )  (Set (Var "x")) ")" )))); end; 




:: deftheorem    defines :::"commutative"::: BCIALG_4:def 9 :  (Bool  "for" (Set (Var "IT")) "being"   ($#l1_bcialg_4 :::"BCK-Algebra_with_Condition(S)":::) "holds"   (Bool  "("  (Bool (Set (Var "IT")) "is"   ($#v3_bcialg_4 :::"commutative"::: )  ) "iff" (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT")) "holds"  (Bool (Set (Set (Var "x"))  ($#k1_bcialg_1 :::"\"::: )  (Set  "(" (Set (Var "x"))  ($#k1_bcialg_1 :::"\"::: )  (Set (Var "y")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "y"))  ($#k1_bcialg_1 :::"\"::: )  (Set  "(" (Set (Var "y"))  ($#k1_bcialg_1 :::"\"::: )  (Set (Var "x")) ")" ))))  ")" )); 
 registration
cluster  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v3_bcialg_1 :::"being_B"::: )     ($#v4_bcialg_1 :::"being_C"::: )     ($#v5_bcialg_1 :::"being_I"::: )     ($#v7_bcialg_1 :::"being_BCI-4"::: )     ($#v8_bcialg_1 :::"being_BCK-5"::: )     ($#v2_bcialg_4 :::"with_condition_S"::: )     ($#v3_bcialg_4 :::"commutative"::: )    for    ($#l1_bcialg_4 :::"BCIStr_1"::: )  ; 
end; 
theorem :: BCIALG_4:42 (Bool  "for" (Set (Var "X")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_bcialg_4 :::"BCIStr_1"::: )   "holds"   (Bool  "("  (Bool (Set (Var "X")) "is"   ($#v3_bcialg_4 :::"commutative"::: )    ($#l1_bcialg_4 :::"BCK-Algebra_with_Condition(S)":::)) "iff" (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "holds"   (Bool  "("  (Bool (Set (Set (Var "x"))  ($#k1_bcialg_1 :::"\"::: )  (Set  "(" (Set  "("  ($#k4_struct_0 :::"0."::: )  (Set (Var "X")) ")" )  ($#k1_bcialg_1 :::"\"::: )  (Set (Var "y")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "x"))) & (Bool (Set (Set  "(" (Set (Var "x"))  ($#k1_bcialg_1 :::"\"::: )  (Set (Var "z")) ")" )  ($#k1_bcialg_1 :::"\"::: )  (Set  "(" (Set (Var "x"))  ($#k1_bcialg_1 :::"\"::: )  (Set (Var "y")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "y"))  ($#k1_bcialg_1 :::"\"::: )  (Set (Var "z")) ")" )  ($#k1_bcialg_1 :::"\"::: )  (Set  "(" (Set (Var "y"))  ($#k1_bcialg_1 :::"\"::: )  (Set (Var "x")) ")" ))) & (Bool (Set (Set  "(" (Set (Var "x"))  ($#k1_bcialg_1 :::"\"::: )  (Set (Var "y")) ")" )  ($#k1_bcialg_1 :::"\"::: )  (Set (Var "z")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "x"))  ($#k1_bcialg_1 :::"\"::: )  (Set  "(" (Set (Var "y"))  ($#k1_bcialg_4 :::"*"::: )  (Set (Var "z")) ")" )))  ")" ))  ")" )) ; 
 
theorem :: BCIALG_4:43 (Bool  "for" (Set (Var "X")) "being"   ($#v3_bcialg_4 :::"commutative"::: )    ($#l1_bcialg_4 :::"BCK-Algebra_with_Condition(S)":::)  (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X"))  "st" (Bool (Bool (Set (Var "a")) "is"   ($#v4_bcialg_2 :::"greatest"::: )  )) "holds"  (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "holds"  (Bool (Set (Set (Var "x"))  ($#k1_bcialg_4 :::"*"::: )  (Set (Var "y")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k1_bcialg_1 :::"\"::: )  (Set  "(" (Set  "(" (Set (Var "a"))  ($#k1_bcialg_1 :::"\"::: )  (Set (Var "x")) ")" )  ($#k1_bcialg_1 :::"\"::: )  (Set (Var "y")) ")" )))))) ; 
 definitionlet "X" be   ($#l2_bcialg_1 :::"BCI-algebra":::); let "a" be   ($#m1_subset_1 :::"Element":::) "of" (Set (Const "X")); func  :::"Initial_section"::: "a" ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_subset_1 :::"Subset":::) "of" "X" equals :: BCIALG_4:def 10  "{"  (Set (Var "t")) where t "is"   ($#m1_subset_1 :::"Element":::) "of" "X" : (Bool (Set (Var "t"))  ($#r1_bcialg_1 :::"<="::: )  "a")  "}"  ; end; 






:: deftheorem    defines :::"Initial_section"::: BCIALG_4:def 10 :  (Bool  "for" (Set (Var "X")) "being"   ($#l2_bcialg_1 :::"BCI-algebra":::)  (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "holds"  (Bool (Set   ($#k8_bcialg_4 :::"Initial_section"::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )   "{"  (Set (Var "t")) where t "is"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) : (Bool (Set (Var "t"))  ($#r1_bcialg_1 :::"<="::: )  (Set (Var "a")))  "}"  ))); 
 
theorem :: BCIALG_4:44 (Bool  "for" (Set (Var "X")) "being"   ($#v3_bcialg_4 :::"commutative"::: )    ($#l1_bcialg_4 :::"BCK-Algebra_with_Condition(S)":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X"))  "st" (Bool (Bool (Set   ($#k3_bcialg_4 :::"Condition_S"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) ")" )  ($#r1_tarski :::"c="::: )  (Set   ($#k8_bcialg_4 :::"Initial_section"::: )  (Set (Var "c"))))) "holds"  (Bool  "for" (Set (Var "x")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k3_bcialg_4 :::"Condition_S"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) "holds"  (Bool (Set (Var "x"))  ($#r1_bcialg_1 :::"<="::: )  (Set (Set (Var "c"))  ($#k1_bcialg_1 :::"\"::: )  (Set  "(" (Set  "(" (Set (Var "c"))  ($#k1_bcialg_1 :::"\"::: )  (Set (Var "a")) ")" )  ($#k1_bcialg_1 :::"\"::: )  (Set (Var "b")) ")" )))))) ; 
 definitionlet "IT" be   ($#l1_bcialg_4 :::"BCK-Algebra_with_Condition(S)":::); attr "IT" is  :::"positive-implicative":::  means :: BCIALG_4:def 11 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Element":::) "of" "IT" "holds"  (Bool (Set (Set  "(" (Set (Var "x"))  ($#k1_bcialg_1 :::"\"::: )  (Set (Var "y")) ")" )  ($#k1_bcialg_1 :::"\"::: )  (Set (Var "y")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "x"))  ($#k1_bcialg_1 :::"\"::: )  (Set (Var "y"))))); end; 




:: deftheorem    defines :::"positive-implicative"::: BCIALG_4:def 11 :  (Bool  "for" (Set (Var "IT")) "being"   ($#l1_bcialg_4 :::"BCK-Algebra_with_Condition(S)":::) "holds"   (Bool  "("  (Bool (Set (Var "IT")) "is"   ($#v4_bcialg_4 :::"positive-implicative"::: )  ) "iff" (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT")) "holds"  (Bool (Set (Set  "(" (Set (Var "x"))  ($#k1_bcialg_1 :::"\"::: )  (Set (Var "y")) ")" )  ($#k1_bcialg_1 :::"\"::: )  (Set (Var "y")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "x"))  ($#k1_bcialg_1 :::"\"::: )  (Set (Var "y")))))  ")" )); 
 registration
cluster  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v3_bcialg_1 :::"being_B"::: )     ($#v4_bcialg_1 :::"being_C"::: )     ($#v5_bcialg_1 :::"being_I"::: )     ($#v7_bcialg_1 :::"being_BCI-4"::: )     ($#v8_bcialg_1 :::"being_BCK-5"::: )     ($#v2_bcialg_4 :::"with_condition_S"::: )     ($#v4_bcialg_4 :::"positive-implicative"::: )    for    ($#l1_bcialg_4 :::"BCIStr_1"::: )  ; 
end; 
theorem :: BCIALG_4:45 (Bool  "for" (Set (Var "X")) "being"   ($#l1_bcialg_4 :::"BCK-Algebra_with_Condition(S)":::) "holds"   (Bool  "("  (Bool (Set (Var "X")) "is"   ($#v4_bcialg_4 :::"positive-implicative"::: )  ) "iff" (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "holds"  (Bool (Set (Set (Var "x"))  ($#k1_bcialg_4 :::"*"::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Var "x"))))  ")" )) ; 
 
theorem :: BCIALG_4:46 (Bool  "for" (Set (Var "X")) "being"   ($#l1_bcialg_4 :::"BCK-Algebra_with_Condition(S)":::) "holds"   (Bool  "("  (Bool (Set (Var "X")) "is"   ($#v4_bcialg_4 :::"positive-implicative"::: )  ) "iff" (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X"))  "st" (Bool (Bool (Set (Var "x"))  ($#r1_bcialg_1 :::"<="::: )  (Set (Var "y")))) "holds"  (Bool (Set (Set (Var "x"))  ($#k1_bcialg_4 :::"*"::: )  (Set (Var "y")))  ($#r1_hidden :::"="::: )  (Set (Var "y"))))  ")" )) ; 
 
theorem :: BCIALG_4:47 (Bool  "for" (Set (Var "X")) "being"   ($#l1_bcialg_4 :::"BCK-Algebra_with_Condition(S)":::) "holds"   (Bool  "("  (Bool (Set (Var "X")) "is"   ($#v4_bcialg_4 :::"positive-implicative"::: )  ) "iff" (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "holds"  (Bool (Set (Set  "(" (Set (Var "x"))  ($#k1_bcialg_4 :::"*"::: )  (Set (Var "y")) ")" )  ($#k1_bcialg_1 :::"\"::: )  (Set (Var "z")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "x"))  ($#k1_bcialg_1 :::"\"::: )  (Set (Var "z")) ")" )  ($#k1_bcialg_4 :::"*"::: )  (Set  "(" (Set (Var "y"))  ($#k1_bcialg_1 :::"\"::: )  (Set (Var "z")) ")" ))))  ")" )) ; 
 
theorem :: BCIALG_4:48 (Bool  "for" (Set (Var "X")) "being"   ($#l1_bcialg_4 :::"BCK-Algebra_with_Condition(S)":::) "holds"   (Bool  "("  (Bool (Set (Var "X")) "is"   ($#v4_bcialg_4 :::"positive-implicative"::: )  ) "iff" (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "holds"  (Bool (Set (Set (Var "x"))  ($#k1_bcialg_4 :::"*"::: )  (Set (Var "y")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "x"))  ($#k1_bcialg_4 :::"*"::: )  (Set  "(" (Set (Var "y"))  ($#k1_bcialg_1 :::"\"::: )  (Set (Var "x")) ")" ))))  ")" )) ; 
 
theorem :: BCIALG_4:49 (Bool  "for" (Set (Var "X")) "being"   ($#v4_bcialg_4 :::"positive-implicative"::: )    ($#l1_bcialg_4 :::"BCK-Algebra_with_Condition(S)":::)  (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "holds"  (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "x"))  ($#k1_bcialg_1 :::"\"::: )  (Set (Var "y")) ")" )  ($#k1_bcialg_4 :::"*"::: )  (Set  "(" (Set (Var "x"))  ($#k1_bcialg_1 :::"\"::: )  (Set  "(" (Set (Var "x"))  ($#k1_bcialg_1 :::"\"::: )  (Set (Var "y")) ")" ) ")" ))))) ; 
 definitionlet "IT" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_bcialg_4 :::"BCIStr_1"::: )  ; attr "IT" is  :::"being_SB-1":::  means :: BCIALG_4:def 12 (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" "IT" "holds"  (Bool (Set (Set (Var "x"))  ($#k1_bcialg_4 :::"*"::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Var "x")))); attr "IT" is  :::"being_SB-2":::  means :: BCIALG_4:def 13 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Element":::) "of" "IT" "holds"  (Bool (Set (Set (Var "x"))  ($#k1_bcialg_4 :::"*"::: )  (Set (Var "y")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "y"))  ($#k1_bcialg_4 :::"*"::: )  (Set (Var "x"))))); attr "IT" is  :::"being_SB-4":::  means :: BCIALG_4:def 14 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Element":::) "of" "IT" "holds"  (Bool (Set (Set  "(" (Set (Var "x"))  ($#k1_bcialg_1 :::"\"::: )  (Set (Var "y")) ")" )  ($#k1_bcialg_4 :::"*"::: )  (Set (Var "y")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "x"))  ($#k1_bcialg_4 :::"*"::: )  (Set (Var "y"))))); end; 












:: deftheorem    defines :::"being_SB-1"::: BCIALG_4:def 12 :  (Bool  "for" (Set (Var "IT")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_bcialg_4 :::"BCIStr_1"::: )   "holds"   (Bool  "("  (Bool (Set (Var "IT")) "is"   ($#v5_bcialg_4 :::"being_SB-1"::: )  ) "iff" (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT")) "holds"  (Bool (Set (Set (Var "x"))  ($#k1_bcialg_4 :::"*"::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Var "x"))))  ")" )); 
 
:: deftheorem    defines :::"being_SB-2"::: BCIALG_4:def 13 :  (Bool  "for" (Set (Var "IT")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_bcialg_4 :::"BCIStr_1"::: )   "holds"   (Bool  "("  (Bool (Set (Var "IT")) "is"   ($#v6_bcialg_4 :::"being_SB-2"::: )  ) "iff" (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT")) "holds"  (Bool (Set (Set (Var "x"))  ($#k1_bcialg_4 :::"*"::: )  (Set (Var "y")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "y"))  ($#k1_bcialg_4 :::"*"::: )  (Set (Var "x")))))  ")" )); 
 
:: deftheorem    defines :::"being_SB-4"::: BCIALG_4:def 14 :  (Bool  "for" (Set (Var "IT")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_bcialg_4 :::"BCIStr_1"::: )   "holds"   (Bool  "("  (Bool (Set (Var "IT")) "is"   ($#v7_bcialg_4 :::"being_SB-4"::: )  ) "iff" (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT")) "holds"  (Bool (Set (Set  "(" (Set (Var "x"))  ($#k1_bcialg_1 :::"\"::: )  (Set (Var "y")) ")" )  ($#k1_bcialg_4 :::"*"::: )  (Set (Var "y")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "x"))  ($#k1_bcialg_4 :::"*"::: )  (Set (Var "y")))))  ")" )); 
 registration
cluster (Set   ($#k2_bcialg_4 :::"BCI_S-EXAMPLE"::: )  ) ->   ($#v5_bcialg_1 :::"being_I"::: )     ($#v2_bcialg_4 :::"with_condition_S"::: )     ($#v5_bcialg_4 :::"being_SB-1"::: )     ($#v6_bcialg_4 :::"being_SB-2"::: )     ($#v7_bcialg_4 :::"being_SB-4"::: )   ; 
end; registration
cluster  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v5_bcialg_1 :::"being_I"::: )     ($#v1_bcialg_4 :::"strict"::: )     ($#v2_bcialg_4 :::"with_condition_S"::: )     ($#v5_bcialg_4 :::"being_SB-1"::: )     ($#v6_bcialg_4 :::"being_SB-2"::: )     ($#v7_bcialg_4 :::"being_SB-4"::: )    for    ($#l1_bcialg_4 :::"BCIStr_1"::: )  ; 
end; definitionmode semi-Brouwerian-algebra is  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v5_bcialg_1 :::"being_I"::: )     ($#v2_bcialg_4 :::"with_condition_S"::: )     ($#v5_bcialg_4 :::"being_SB-1"::: )     ($#v6_bcialg_4 :::"being_SB-2"::: )     ($#v7_bcialg_4 :::"being_SB-4"::: )     ($#l1_bcialg_4 :::"BCIStr_1"::: )  ; end; 
theorem :: BCIALG_4:50 (Bool  "for" (Set (Var "X")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_bcialg_4 :::"BCIStr_1"::: )   "holds"   (Bool  "("  (Bool (Set (Var "X")) "is"   ($#v4_bcialg_4 :::"positive-implicative"::: )    ($#l1_bcialg_4 :::"BCK-Algebra_with_Condition(S)":::)) "iff" (Bool (Set (Var "X")) "is"   ($#l1_bcialg_4 :::"semi-Brouwerian-algebra":::))  ")" )) ; 
 definitionlet "IT" be   ($#l1_bcialg_4 :::"BCK-Algebra_with_Condition(S)":::); attr "IT" is  :::"implicative":::  means :: BCIALG_4:def 15 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Element":::) "of" "IT" "holds"  (Bool (Set (Set (Var "x"))  ($#k1_bcialg_1 :::"\"::: )  (Set  "(" (Set (Var "y"))  ($#k1_bcialg_1 :::"\"::: )  (Set (Var "x")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "x")))); end; 




:: deftheorem    defines :::"implicative"::: BCIALG_4:def 15 :  (Bool  "for" (Set (Var "IT")) "being"   ($#l1_bcialg_4 :::"BCK-Algebra_with_Condition(S)":::) "holds"   (Bool  "("  (Bool (Set (Var "IT")) "is"   ($#v8_bcialg_4 :::"implicative"::: )  ) "iff" (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT")) "holds"  (Bool (Set (Set (Var "x"))  ($#k1_bcialg_1 :::"\"::: )  (Set  "(" (Set (Var "y"))  ($#k1_bcialg_1 :::"\"::: )  (Set (Var "x")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "x"))))  ")" )); 
 registration
cluster  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v3_bcialg_1 :::"being_B"::: )     ($#v4_bcialg_1 :::"being_C"::: )     ($#v5_bcialg_1 :::"being_I"::: )     ($#v7_bcialg_1 :::"being_BCI-4"::: )     ($#v8_bcialg_1 :::"being_BCK-5"::: )     ($#v2_bcialg_4 :::"with_condition_S"::: )     ($#v8_bcialg_4 :::"implicative"::: )    for    ($#l1_bcialg_4 :::"BCIStr_1"::: )  ; 
end; 
theorem :: BCIALG_4:51 (Bool  "for" (Set (Var "X")) "being"   ($#l1_bcialg_4 :::"BCK-Algebra_with_Condition(S)":::) "holds"   (Bool  "("  (Bool (Set (Var "X")) "is"   ($#v8_bcialg_4 :::"implicative"::: )  ) "iff" (Bool  "("  (Bool (Set (Var "X")) "is"   ($#v3_bcialg_4 :::"commutative"::: )  ) & (Bool (Set (Var "X")) "is"   ($#v4_bcialg_4 :::"positive-implicative"::: )  )  ")" )  ")" )) ; 
 
theorem :: BCIALG_4:52 (Bool  "for" (Set (Var "X")) "being"   ($#l1_bcialg_4 :::"BCK-Algebra_with_Condition(S)":::) "holds"   (Bool  "("  (Bool (Set (Var "X")) "is"   ($#v8_bcialg_4 :::"implicative"::: )  ) "iff" (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "holds"  (Bool (Set (Set (Var "x"))  ($#k1_bcialg_1 :::"\"::: )  (Set  "(" (Set (Var "y"))  ($#k1_bcialg_1 :::"\"::: )  (Set (Var "z")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set (Var "x"))  ($#k1_bcialg_1 :::"\"::: )  (Set (Var "y")) ")" )  ($#k1_bcialg_1 :::"\"::: )  (Set (Var "z")) ")" )  ($#k1_bcialg_4 :::"*"::: )  (Set  "(" (Set (Var "z"))  ($#k1_bcialg_1 :::"\"::: )  (Set  "(" (Set (Var "z"))  ($#k1_bcialg_1 :::"\"::: )  (Set (Var "x")) ")" ) ")" ))))  ")" )) ;