:: BCIIDEAL semantic presentation begin theorem :: BCIIDEAL:1 (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCI-algebra":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "," (Set (Var "u")) "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 "u")) ($#k1_bcialg_1 :::"\"::: ) (Set "(" (Set (Var "z")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "x")) ")" )) ($#r1_bcialg_1 :::"<="::: ) (Set (Set (Var "u")) ($#k1_bcialg_1 :::"\"::: ) (Set "(" (Set (Var "z")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "y")) ")" ))))) ; theorem :: BCIIDEAL:2 (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCI-algebra":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "," (Set (Var "u")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set "(" (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set "(" (Set (Var "y")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "z")) ")" ) ")" ) ($#k1_bcialg_1 :::"\"::: ) (Set "(" (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set "(" (Set (Var "y")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "u")) ")" ) ")" )) ($#r1_bcialg_1 :::"<="::: ) (Set (Set (Var "z")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "u")))))) ; theorem :: BCIIDEAL:3 (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCI-algebra":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "," (Set (Var "u")) "," (Set (Var "v")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set "(" (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set "(" (Set (Var "y")) ($#k1_bcialg_1 :::"\"::: ) (Set "(" (Set (Var "z")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "u")) ")" ) ")" ) ")" ) ($#k1_bcialg_1 :::"\"::: ) (Set "(" (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set "(" (Set (Var "y")) ($#k1_bcialg_1 :::"\"::: ) (Set "(" (Set (Var "z")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "v")) ")" ) ")" ) ")" )) ($#r1_bcialg_1 :::"<="::: ) (Set (Set (Var "v")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "u")))))) ; theorem :: BCIIDEAL:4 (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCI-algebra":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set "(" (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "X")) ")" ) ($#k1_bcialg_1 :::"\"::: ) (Set "(" (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "y")) ")" ) ")" ) ($#k1_bcialg_1 :::"\"::: ) (Set "(" (Set (Var "y")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "x")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "X")))))) ; definitionlet "X" be ($#l2_bcialg_1 :::"BCI-algebra":::); let "a" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "X")); func :::"initial_section"::: "a" -> ($#m1_hidden :::"set"::: ) equals :: BCIIDEAL:def 1 "{" (Set (Var "x")) where x "is" ($#m1_subset_1 :::"Element":::) "of" "X" : (Bool (Set (Var "x")) ($#r1_bcialg_1 :::"<="::: ) "a") "}" ; end; :: deftheorem defines :::"initial_section"::: BCIIDEAL:def 1 : (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 ($#k1_bciideal :::"initial_section"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) "{" (Set (Var "x")) where x "is" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) : (Bool (Set (Var "x")) ($#r1_bcialg_1 :::"<="::: ) (Set (Var "a"))) "}" ))); theorem :: BCIIDEAL:5 (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCI-algebra":::) (Bool "for" (Set (Var "A")) "being" ($#m2_bcialg_1 :::"Ideal"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "a")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "A")) "st" (Bool (Bool (Set (Var "x")) ($#r1_bcialg_1 :::"<="::: ) (Set (Var "a")))) "holds" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))))))) ; theorem :: BCIIDEAL:6 (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCI-algebra":::) (Bool "for" (Set (Var "x")) "," (Set (Var "a")) "," (Set (Var "b")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_bcialg_1 :::"AtomSet"::: ) (Set (Var "X"))) "st" (Bool (Bool (Set (Var "x")) "is" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k7_bcialg_1 :::"BranchV"::: ) (Set (Var "b"))))) "holds" (Bool (Set (Set (Var "a")) ($#k6_bcialg_1 :::"\"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k6_bcialg_1 :::"\"::: ) (Set (Var "b")))))) ; theorem :: BCIIDEAL:7 (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")) (Bool "for" (Set (Var "x")) "," (Set (Var "b")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_bcialg_1 :::"AtomSet"::: ) (Set (Var "X"))) "st" (Bool (Bool (Set (Var "x")) "is" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k7_bcialg_1 :::"BranchV"::: ) (Set (Var "b"))))) "holds" (Bool (Set (Set (Var "a")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "b"))))))) ; theorem :: BCIIDEAL:8 (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCI-algebra":::) (Bool "for" (Set (Var "A")) "being" ($#m2_bcialg_1 :::"Ideal"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "a")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "A")) "holds" (Bool (Set ($#k1_bciideal :::"initial_section"::: ) (Set (Var "a"))) ($#r1_tarski :::"c="::: ) (Set (Var "A")))))) ; theorem :: BCIIDEAL:9 (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCI-algebra":::) "st" (Bool (Bool (Set ($#k5_bcialg_1 :::"AtomSet"::: ) (Set (Var "X"))) "is" ($#m2_bcialg_1 :::"Ideal"::: ) "of" (Set (Var "X")))) "holds" (Bool "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k4_bcialg_1 :::"BCK-part"::: ) (Set (Var "X"))) (Bool "for" (Set (Var "a")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_bcialg_1 :::"AtomSet"::: ) (Set (Var "X"))) "st" (Bool (Bool (Set (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "a"))) ($#r2_hidden :::"in"::: ) (Set ($#k5_bcialg_1 :::"AtomSet"::: ) (Set (Var "X"))))) "holds" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "X"))))))) ; theorem :: BCIIDEAL:10 (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCI-algebra":::) "st" (Bool (Bool (Set ($#k5_bcialg_1 :::"AtomSet"::: ) (Set (Var "X"))) "is" ($#m2_bcialg_1 :::"Ideal"::: ) "of" (Set (Var "X")))) "holds" (Bool (Set ($#k5_bcialg_1 :::"AtomSet"::: ) (Set (Var "X"))) "is" ($#v12_bcialg_1 :::"closed"::: ) ($#m2_bcialg_1 :::"Ideal"::: ) "of" (Set (Var "X")))) ; definitionlet "X" be ($#l2_bcialg_1 :::"BCI-algebra":::); let "I" be ($#m2_bcialg_1 :::"Ideal"::: ) "of" (Set (Const "X")); attr "I" is :::"positive"::: means :: BCIIDEAL:def 2 (Bool "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"Element"::: ) "of" "I" "holds" (Bool (Set (Var "x")) "is" ($#v1_bcialg_2 :::"positive"::: ) )); end; :: deftheorem defines :::"positive"::: BCIIDEAL:def 2 : (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCI-algebra":::) (Bool "for" (Set (Var "I")) "being" ($#m2_bcialg_1 :::"Ideal"::: ) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "I")) "is" ($#v1_bciideal :::"positive"::: ) ) "iff" (Bool "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "I")) "holds" (Bool (Set (Var "x")) "is" ($#v1_bcialg_2 :::"positive"::: ) )) ")" ))); theorem :: BCIIDEAL:11 (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCK-algebra":::) (Bool "for" (Set (Var "A")) "," (Set (Var "I")) "being" ($#m2_bcialg_1 :::"Ideal"::: ) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Set (Var "A")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "I"))) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "X")) ")" ) ($#k1_tarski :::"}"::: ) )) "iff" (Bool "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "A")) (Bool "for" (Set (Var "y")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "I")) "holds" (Bool (Set (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Var "x"))))) ")" ))) ; theorem :: BCIIDEAL:12 (Bool "for" (Set (Var "X")) "being" ($#v13_bcialg_1 :::"associative"::: ) ($#l2_bcialg_1 :::"BCI-algebra":::) (Bool "for" (Set (Var "A")) "being" ($#m2_bcialg_1 :::"Ideal"::: ) "of" (Set (Var "X")) "holds" (Bool (Set (Var "A")) "is" ($#v12_bcialg_1 :::"closed"::: ) ))) ; theorem :: BCIIDEAL:13 (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCI-algebra":::) (Bool "for" (Set (Var "A")) "being" ($#m2_bcialg_1 :::"Ideal"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "X")) "is" ($#v14_bcialg_1 :::"quasi-associative"::: ) )) "holds" (Bool (Set (Var "A")) "is" ($#v12_bcialg_1 :::"closed"::: ) ))) ; begin definitionlet "X" be ($#l2_bcialg_1 :::"BCI-algebra":::); let "IT" be ($#m2_bcialg_1 :::"Ideal"::: ) "of" (Set (Const "X")); attr "IT" is :::"associative"::: means :: BCIIDEAL:def 3 (Bool "(" (Bool (Set ($#k4_struct_0 :::"0."::: ) "X") ($#r2_hidden :::"in"::: ) "IT") & (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" "X" "st" (Bool (Bool (Set (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set "(" (Set (Var "y")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "z")) ")" )) ($#r2_hidden :::"in"::: ) "IT") & (Bool (Set (Set (Var "y")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "z"))) ($#r2_hidden :::"in"::: ) "IT")) "holds" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) "IT") ")" ) ")" ); end; :: deftheorem defines :::"associative"::: BCIIDEAL:def 3 : (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCI-algebra":::) (Bool "for" (Set (Var "IT")) "being" ($#m2_bcialg_1 :::"Ideal"::: ) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v2_bciideal :::"associative"::: ) ) "iff" (Bool "(" (Bool (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "X"))) ($#r2_hidden :::"in"::: ) (Set (Var "IT"))) & (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set "(" (Set (Var "y")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "z")) ")" )) ($#r2_hidden :::"in"::: ) (Set (Var "IT"))) & (Bool (Set (Set (Var "y")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "z"))) ($#r2_hidden :::"in"::: ) (Set (Var "IT")))) "holds" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "IT"))) ")" ) ")" ) ")" ))); registrationlet "X" be ($#l2_bcialg_1 :::"BCI-algebra":::); cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v2_bciideal :::"associative"::: ) for ($#m2_bcialg_1 :::"Ideal"::: ) "of" "X"; end; definitionlet "X" be ($#l2_bcialg_1 :::"BCI-algebra":::); mode :::"associative-ideal"::: "of" "X" -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" "X" means :: BCIIDEAL:def 4 (Bool "(" (Bool (Set ($#k4_struct_0 :::"0."::: ) "X") ($#r2_hidden :::"in"::: ) it) & (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" "X" "st" (Bool (Bool (Set (Set "(" (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "y")) ")" ) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "z"))) ($#r2_hidden :::"in"::: ) it) & (Bool (Set (Set (Var "y")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "z"))) ($#r2_hidden :::"in"::: ) it)) "holds" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) it) ")" ) ")" ); end; :: deftheorem defines :::"associative-ideal"::: BCIIDEAL:def 4 : (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCI-algebra":::) (Bool "for" (Set (Var "b2")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "b2")) "is" ($#m1_bciideal :::"associative-ideal"::: ) "of" (Set (Var "X"))) "iff" (Bool "(" (Bool (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "X"))) ($#r2_hidden :::"in"::: ) (Set (Var "b2"))) & (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Set "(" (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "y")) ")" ) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "z"))) ($#r2_hidden :::"in"::: ) (Set (Var "b2"))) & (Bool (Set (Set (Var "y")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "z"))) ($#r2_hidden :::"in"::: ) (Set (Var "b2")))) "holds" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "b2"))) ")" ) ")" ) ")" ))); theorem :: BCIIDEAL:14 (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCI-algebra":::) (Bool "for" (Set (Var "X1")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "X1")) "is" ($#m1_bciideal :::"associative-ideal"::: ) "of" (Set (Var "X")))) "holds" (Bool (Set (Var "X1")) "is" ($#m2_bcialg_1 :::"Ideal"::: ) "of" (Set (Var "X"))))) ; theorem :: BCIIDEAL:15 (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCI-algebra":::) (Bool "for" (Set (Var "I")) "being" ($#m2_bcialg_1 :::"Ideal"::: ) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "I")) "is" ($#m1_bciideal :::"associative-ideal"::: ) "of" (Set (Var "X"))) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Set "(" (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "y")) ")" ) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "z"))) ($#r2_hidden :::"in"::: ) (Set (Var "I")))) "holds" (Bool (Set (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set "(" (Set (Var "y")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "z")) ")" )) ($#r2_hidden :::"in"::: ) (Set (Var "I")))) ")" ))) ; theorem :: BCIIDEAL:16 (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCI-algebra":::) (Bool "for" (Set (Var "I")) "being" ($#m2_bcialg_1 :::"Ideal"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "I")) "is" ($#m1_bciideal :::"associative-ideal"::: ) "of" (Set (Var "X")))) "holds" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set "(" (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "X")) ")" ) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "x")) ")" )) ($#r2_hidden :::"in"::: ) (Set (Var "I")))))) ; theorem :: BCIIDEAL:17 (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCI-algebra":::) (Bool "for" (Set (Var "I")) "being" ($#m2_bcialg_1 :::"Ideal"::: ) "of" (Set (Var "X")) "st" (Bool (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set "(" (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "X")) ")" ) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "x")) ")" )) ($#r2_hidden :::"in"::: ) (Set (Var "I"))) ")" )) "holds" (Bool (Set (Var "I")) "is" ($#v12_bcialg_1 :::"closed"::: ) ($#m2_bcialg_1 :::"Ideal"::: ) "of" (Set (Var "X"))))) ; definitionlet "X" be ($#l2_bcialg_1 :::"BCI-algebra":::); mode :::"p-ideal"::: "of" "X" -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" "X" means :: BCIIDEAL:def 5 (Bool "(" (Bool (Set ($#k4_struct_0 :::"0."::: ) "X") ($#r2_hidden :::"in"::: ) it) & (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" "X" "st" (Bool (Bool (Set (Set "(" (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "z")) ")" ) ($#k1_bcialg_1 :::"\"::: ) (Set "(" (Set (Var "y")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "z")) ")" )) ($#r2_hidden :::"in"::: ) it) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) it)) "holds" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) it) ")" ) ")" ); end; :: deftheorem defines :::"p-ideal"::: BCIIDEAL:def 5 : (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCI-algebra":::) (Bool "for" (Set (Var "b2")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "b2")) "is" ($#m2_bciideal :::"p-ideal"::: ) "of" (Set (Var "X"))) "iff" (Bool "(" (Bool (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "X"))) ($#r2_hidden :::"in"::: ) (Set (Var "b2"))) & (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Set "(" (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "z")) ")" ) ($#k1_bcialg_1 :::"\"::: ) (Set "(" (Set (Var "y")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "z")) ")" )) ($#r2_hidden :::"in"::: ) (Set (Var "b2"))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "b2")))) "holds" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "b2"))) ")" ) ")" ) ")" ))); theorem :: BCIIDEAL:18 (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCI-algebra":::) (Bool "for" (Set (Var "X1")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "X1")) "is" ($#m2_bciideal :::"p-ideal"::: ) "of" (Set (Var "X")))) "holds" (Bool (Set (Var "X1")) "is" ($#m2_bcialg_1 :::"Ideal"::: ) "of" (Set (Var "X"))))) ; theorem :: BCIIDEAL:19 (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCI-algebra":::) (Bool "for" (Set (Var "I")) "being" ($#m2_bcialg_1 :::"Ideal"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "I")) "is" ($#m2_bciideal :::"p-ideal"::: ) "of" (Set (Var "X")))) "holds" (Bool (Set ($#k4_bcialg_1 :::"BCK-part"::: ) (Set (Var "X"))) ($#r1_tarski :::"c="::: ) (Set (Var "I"))))) ; theorem :: BCIIDEAL:20 (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCI-algebra":::) "holds" (Bool (Set ($#k4_bcialg_1 :::"BCK-part"::: ) (Set (Var "X"))) "is" ($#m2_bciideal :::"p-ideal"::: ) "of" (Set (Var "X")))) ; theorem :: BCIIDEAL:21 (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCI-algebra":::) (Bool "for" (Set (Var "I")) "being" ($#m2_bcialg_1 :::"Ideal"::: ) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "I")) "is" ($#m2_bciideal :::"p-ideal"::: ) "of" (Set (Var "X"))) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "I"))) & (Bool (Set (Var "x")) ($#r1_bcialg_1 :::"<="::: ) (Set (Var "y")))) "holds" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "I")))) ")" ))) ; theorem :: BCIIDEAL:22 (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCI-algebra":::) (Bool "for" (Set (Var "I")) "being" ($#m2_bcialg_1 :::"Ideal"::: ) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "I")) "is" ($#m2_bciideal :::"p-ideal"::: ) "of" (Set (Var "X"))) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Set "(" (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "z")) ")" ) ($#k1_bcialg_1 :::"\"::: ) (Set "(" (Set (Var "y")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "z")) ")" )) ($#r2_hidden :::"in"::: ) (Set (Var "I")))) "holds" (Bool (Set (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "y"))) ($#r2_hidden :::"in"::: ) (Set (Var "I")))) ")" ))) ; begin definitionlet "X" be ($#l2_bcialg_1 :::"BCK-algebra":::); let "IT" be ($#m2_bcialg_1 :::"Ideal"::: ) "of" (Set (Const "X")); attr "IT" is :::"commutative"::: means :: BCIIDEAL:def 6 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" "X" "st" (Bool (Bool (Set (Set "(" (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "y")) ")" ) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "z"))) ($#r2_hidden :::"in"::: ) "IT") & (Bool (Set (Var "z")) ($#r2_hidden :::"in"::: ) "IT")) "holds" (Bool (Set (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set "(" (Set (Var "y")) ($#k1_bcialg_1 :::"\"::: ) (Set "(" (Set (Var "y")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "x")) ")" ) ")" )) ($#r2_hidden :::"in"::: ) "IT")); end; :: deftheorem defines :::"commutative"::: BCIIDEAL:def 6 : (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCK-algebra":::) (Bool "for" (Set (Var "IT")) "being" ($#m2_bcialg_1 :::"Ideal"::: ) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v3_bciideal :::"commutative"::: ) ) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Set "(" (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "y")) ")" ) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "z"))) ($#r2_hidden :::"in"::: ) (Set (Var "IT"))) & (Bool (Set (Var "z")) ($#r2_hidden :::"in"::: ) (Set (Var "IT")))) "holds" (Bool (Set (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set "(" (Set (Var "y")) ($#k1_bcialg_1 :::"\"::: ) (Set "(" (Set (Var "y")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "x")) ")" ) ")" )) ($#r2_hidden :::"in"::: ) (Set (Var "IT")))) ")" ))); registrationlet "X" be ($#l2_bcialg_1 :::"BCK-algebra":::); cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v3_bciideal :::"commutative"::: ) for ($#m2_bcialg_1 :::"Ideal"::: ) "of" "X"; end; theorem :: BCIIDEAL:23 (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCK-algebra":::) "holds" (Bool (Set ($#k4_bcialg_1 :::"BCK-part"::: ) (Set (Var "X"))) "is" ($#v3_bciideal :::"commutative"::: ) ($#m2_bcialg_1 :::"Ideal"::: ) "of" (Set (Var "X")))) ; theorem :: BCIIDEAL:24 (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCK-algebra":::) "st" (Bool (Bool (Set (Var "X")) "is" ($#v19_bcialg_1 :::"p-Semisimple"::: ) ($#l2_bcialg_1 :::"BCI-algebra":::))) "holds" (Bool (Set ($#k1_tarski :::"{"::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "X")) ")" ) ($#k1_tarski :::"}"::: ) ) "is" ($#v3_bciideal :::"commutative"::: ) ($#m2_bcialg_1 :::"Ideal"::: ) "of" (Set (Var "X")))) ; theorem :: BCIIDEAL:25 (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCK-algebra":::) "holds" (Bool (Set ($#k4_bcialg_1 :::"BCK-part"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X"))))) ; theorem :: BCIIDEAL:26 (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCI-algebra":::) "st" (Bool (Bool "(" "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCI-algebra":::) (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_1 :::"\"::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "y"))))) ")" )) "holds" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set ($#k4_bcialg_1 :::"BCK-part"::: ) (Set (Var "X"))))) ; theorem :: BCIIDEAL:27 (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCI-algebra":::) "st" (Bool (Bool "(" "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCI-algebra":::) (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_1 :::"\"::: ) (Set "(" (Set (Var "y")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "x")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "x")))) ")" )) "holds" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set ($#k4_bcialg_1 :::"BCK-part"::: ) (Set (Var "X"))))) ; theorem :: BCIIDEAL:28 (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCI-algebra":::) "st" (Bool (Bool "(" "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCI-algebra":::) (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_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")) ")" )))) ")" )) "holds" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set ($#k4_bcialg_1 :::"BCK-part"::: ) (Set (Var "X"))))) ; theorem :: BCIIDEAL:29 (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCI-algebra":::) "st" (Bool (Bool "(" "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCI-algebra":::) (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 "y"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "z")) ")" ) ($#k1_bcialg_1 :::"\"::: ) (Set "(" (Set (Var "y")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "z")) ")" )))) ")" )) "holds" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set ($#k4_bcialg_1 :::"BCK-part"::: ) (Set (Var "X"))))) ; theorem :: BCIIDEAL:30 (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCI-algebra":::) "st" (Bool (Bool "(" "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCI-algebra":::) (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_1 :::"\"::: ) (Set "(" (Set (Var "y")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "x")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "y"))))) ")" )) "holds" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set ($#k4_bcialg_1 :::"BCK-part"::: ) (Set (Var "X"))))) ; theorem :: BCIIDEAL:31 (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCI-algebra":::) "st" (Bool (Bool "(" "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCI-algebra":::) (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_1 :::"\"::: ) (Set "(" (Set "(" (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "y")) ")" ) ($#k1_bcialg_1 :::"\"::: ) (Set "(" (Set (Var "y")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "x")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "X"))))) ")" )) "holds" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set ($#k4_bcialg_1 :::"BCK-part"::: ) (Set (Var "X"))))) ; theorem :: BCIIDEAL:32 (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCK-algebra":::) "holds" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X"))) "is" ($#v3_bciideal :::"commutative"::: ) ($#m2_bcialg_1 :::"Ideal"::: ) "of" (Set (Var "X")))) ; theorem :: BCIIDEAL:33 (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCK-algebra":::) (Bool "for" (Set (Var "I")) "being" ($#m2_bcialg_1 :::"Ideal"::: ) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "I")) "is" ($#v3_bciideal :::"commutative"::: ) ($#m2_bcialg_1 :::"Ideal"::: ) "of" (Set (Var "X"))) "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"))) ($#r2_hidden :::"in"::: ) (Set (Var "I")))) "holds" (Bool (Set (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set "(" (Set (Var "y")) ($#k1_bcialg_1 :::"\"::: ) (Set "(" (Set (Var "y")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "x")) ")" ) ")" )) ($#r2_hidden :::"in"::: ) (Set (Var "I")))) ")" ))) ; theorem :: BCIIDEAL:34 (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCK-algebra":::) (Bool "for" (Set (Var "I")) "," (Set (Var "A")) "being" ($#m2_bcialg_1 :::"Ideal"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "I")) ($#r1_tarski :::"c="::: ) (Set (Var "A"))) & (Bool (Set (Var "I")) "is" ($#v3_bciideal :::"commutative"::: ) ($#m2_bcialg_1 :::"Ideal"::: ) "of" (Set (Var "X")))) "holds" (Bool (Set (Var "A")) "is" ($#v3_bciideal :::"commutative"::: ) ($#m2_bcialg_1 :::"Ideal"::: ) "of" (Set (Var "X"))))) ; theorem :: BCIIDEAL:35 (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCK-algebra":::) "holds" (Bool "(" (Bool "(" "for" (Set (Var "I")) "being" ($#m2_bcialg_1 :::"Ideal"::: ) "of" (Set (Var "X")) "holds" (Bool (Set (Var "I")) "is" ($#v3_bciideal :::"commutative"::: ) ($#m2_bcialg_1 :::"Ideal"::: ) "of" (Set (Var "X"))) ")" ) "iff" (Bool (Set ($#k1_tarski :::"{"::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "X")) ")" ) ($#k1_tarski :::"}"::: ) ) "is" ($#v3_bciideal :::"commutative"::: ) ($#m2_bcialg_1 :::"Ideal"::: ) "of" (Set (Var "X"))) ")" )) ; theorem :: BCIIDEAL:36 (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCK-algebra":::) "holds" (Bool "(" (Bool (Set ($#k1_tarski :::"{"::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "X")) ")" ) ($#k1_tarski :::"}"::: ) ) "is" ($#v3_bciideal :::"commutative"::: ) ($#m2_bcialg_1 :::"Ideal"::: ) "of" (Set (Var "X"))) "iff" (Bool (Set (Var "X")) "is" ($#v1_bcialg_3 :::"commutative"::: ) ($#l2_bcialg_1 :::"BCK-algebra":::)) ")" )) ; theorem :: BCIIDEAL:37 (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCK-algebra":::) "holds" (Bool "(" (Bool (Set (Var "X")) "is" ($#v1_bcialg_3 :::"commutative"::: ) ($#l2_bcialg_1 :::"BCK-algebra":::)) "iff" (Bool "for" (Set (Var "I")) "being" ($#m2_bcialg_1 :::"Ideal"::: ) "of" (Set (Var "X")) "holds" (Bool (Set (Var "I")) "is" ($#v3_bciideal :::"commutative"::: ) ($#m2_bcialg_1 :::"Ideal"::: ) "of" (Set (Var "X")))) ")" )) ; theorem :: BCIIDEAL:38 (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCK-algebra":::) "holds" (Bool "(" (Bool (Set ($#k1_tarski :::"{"::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "X")) ")" ) ($#k1_tarski :::"}"::: ) ) "is" ($#v3_bciideal :::"commutative"::: ) ($#m2_bcialg_1 :::"Ideal"::: ) "of" (Set (Var "X"))) "iff" (Bool "for" (Set (Var "I")) "being" ($#m2_bcialg_1 :::"Ideal"::: ) "of" (Set (Var "X")) "holds" (Bool (Set (Var "I")) "is" ($#v3_bciideal :::"commutative"::: ) ($#m2_bcialg_1 :::"Ideal"::: ) "of" (Set (Var "X")))) ")" )) ; theorem :: BCIIDEAL:39 (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCK-algebra":::) (Bool "for" (Set (Var "I")) "being" ($#m2_bcialg_1 :::"Ideal"::: ) "of" (Set (Var "X")) (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 "(" (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "y")) ")" )) ($#r2_hidden :::"in"::: ) (Set (Var "I")))) "holds" (Bool "(" (Bool (Set (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set "(" (Set "(" (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "y")) ")" ) ($#k1_bcialg_1 :::"\"::: ) (Set "(" (Set "(" (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "y")) ")" ) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "x")) ")" ) ")" )) ($#r2_hidden :::"in"::: ) (Set (Var "I"))) & (Bool (Set (Set "(" (Set (Var "y")) ($#k1_bcialg_1 :::"\"::: ) (Set "(" (Set (Var "y")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "x")) ")" ) ")" ) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "x"))) ($#r2_hidden :::"in"::: ) (Set (Var "I"))) & (Bool (Set (Set "(" (Set (Var "y")) ($#k1_bcialg_1 :::"\"::: ) (Set "(" (Set (Var "y")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "x")) ")" ) ")" ) ($#k1_bcialg_1 :::"\"::: ) (Set "(" (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "y")) ")" )) ($#r2_hidden :::"in"::: ) (Set (Var "I"))) ")" )))) ; theorem :: BCIIDEAL:40 (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCK-algebra":::) "holds" (Bool "(" (Bool (Set ($#k1_tarski :::"{"::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "X")) ")" ) ($#k1_tarski :::"}"::: ) ) "is" ($#v3_bciideal :::"commutative"::: ) ($#m2_bcialg_1 :::"Ideal"::: ) "of" (Set (Var "X"))) "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_1 :::"\"::: ) (Set "(" (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "y")) ")" )) ($#r1_bcialg_1 :::"<="::: ) (Set (Set (Var "y")) ($#k1_bcialg_1 :::"\"::: ) (Set "(" (Set (Var "y")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "x")) ")" )))) ")" )) ; theorem :: BCIIDEAL:41 (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCK-algebra":::) "holds" (Bool "(" (Bool (Set ($#k1_tarski :::"{"::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "X")) ")" ) ($#k1_tarski :::"}"::: ) ) "is" ($#v3_bciideal :::"commutative"::: ) ($#m2_bcialg_1 :::"Ideal"::: ) "of" (Set (Var "X"))) "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_1 :::"\"::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set "(" (Set (Var "y")) ($#k1_bcialg_1 :::"\"::: ) (Set "(" (Set (Var "y")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "x")) ")" ) ")" )))) ")" )) ; theorem :: BCIIDEAL:42 (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCK-algebra":::) "holds" (Bool "(" (Bool (Set ($#k1_tarski :::"{"::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "X")) ")" ) ($#k1_tarski :::"}"::: ) ) "is" ($#v3_bciideal :::"commutative"::: ) ($#m2_bcialg_1 :::"Ideal"::: ) "of" (Set (Var "X"))) "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_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 "(" (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set "(" (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "y")) ")" ) ")" ) ")" )))) ")" )) ; theorem :: BCIIDEAL:43 (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCK-algebra":::) "holds" (Bool "(" (Bool (Set ($#k1_tarski :::"{"::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "X")) ")" ) ($#k1_tarski :::"}"::: ) ) "is" ($#v3_bciideal :::"commutative"::: ) ($#m2_bcialg_1 :::"Ideal"::: ) "of" (Set (Var "X"))) "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 (Var "x")) ($#r1_hidden :::"="::: ) (Set (Set (Var "y")) ($#k1_bcialg_1 :::"\"::: ) (Set "(" (Set (Var "y")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "x")) ")" )))) ")" )) ; theorem :: BCIIDEAL:44 (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCK-algebra":::) "st" (Bool (Bool (Set ($#k1_tarski :::"{"::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "X")) ")" ) ($#k1_tarski :::"}"::: ) ) "is" ($#v3_bciideal :::"commutative"::: ) ($#m2_bcialg_1 :::"Ideal"::: ) "of" (Set (Var "X")))) "holds" (Bool "(" (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Var "x"))) "iff" (Bool (Set (Set (Var "y")) ($#k1_bcialg_1 :::"\"::: ) (Set "(" (Set (Var "y")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "x")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "X")))) ")" ) ")" ) & (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 (Var "x")))) "holds" (Bool (Set (Set (Var "y")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Var "y"))) ")" ) & (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "y")) ($#r1_bcialg_1 :::"<="::: ) (Set (Var "a")))) "holds" (Bool (Set (Set "(" (Set (Var "a")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "x")) ")" ) ($#k1_bcialg_1 :::"\"::: ) (Set "(" (Set (Var "a")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "y")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "y")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "x")))) ")" ) & (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set "(" (Set (Var "y")) ($#k1_bcialg_1 :::"\"::: ) (Set "(" (Set (Var "y")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "x")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "y")))) & (Bool (Set (Set "(" (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "y")) ")" ) ($#k1_bcialg_1 :::"\"::: ) (Set "(" (Set "(" (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "y")) ")" ) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "x")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "y")))) ")" ) ")" ) & (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "x")) ($#r1_bcialg_1 :::"<="::: ) (Set (Var "a")))) "holds" (Bool (Set (Set "(" (Set (Var "a")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "y")) ")" ) ($#k1_bcialg_1 :::"\"::: ) (Set "(" (Set "(" (Set (Var "a")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "y")) ")" ) ($#k1_bcialg_1 :::"\"::: ) (Set "(" (Set (Var "a")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "x")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "y")) ")" ) ($#k1_bcialg_1 :::"\"::: ) (Set "(" (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "y")) ")" ))) ")" ) ")" )) ; theorem :: BCIIDEAL:45 (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCK-algebra":::) "holds" (Bool "(" (Bool "(" "for" (Set (Var "I")) "being" ($#m2_bcialg_1 :::"Ideal"::: ) "of" (Set (Var "X")) "holds" (Bool (Set (Var "I")) "is" ($#v3_bciideal :::"commutative"::: ) ($#m2_bcialg_1 :::"Ideal"::: ) "of" (Set (Var "X"))) ")" ) "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_1 :::"\"::: ) (Set "(" (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "y")) ")" )) ($#r1_bcialg_1 :::"<="::: ) (Set (Set (Var "y")) ($#k1_bcialg_1 :::"\"::: ) (Set "(" (Set (Var "y")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "x")) ")" )))) ")" )) ; theorem :: BCIIDEAL:46 (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCK-algebra":::) "holds" (Bool "(" (Bool "(" "for" (Set (Var "I")) "being" ($#m2_bcialg_1 :::"Ideal"::: ) "of" (Set (Var "X")) "holds" (Bool (Set (Var "I")) "is" ($#v3_bciideal :::"commutative"::: ) ($#m2_bcialg_1 :::"Ideal"::: ) "of" (Set (Var "X"))) ")" ) "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_1 :::"\"::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set "(" (Set (Var "y")) ($#k1_bcialg_1 :::"\"::: ) (Set "(" (Set (Var "y")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "x")) ")" ) ")" )))) ")" )) ; theorem :: BCIIDEAL:47 (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCK-algebra":::) "holds" (Bool "(" (Bool "(" "for" (Set (Var "I")) "being" ($#m2_bcialg_1 :::"Ideal"::: ) "of" (Set (Var "X")) "holds" (Bool (Set (Var "I")) "is" ($#v3_bciideal :::"commutative"::: ) ($#m2_bcialg_1 :::"Ideal"::: ) "of" (Set (Var "X"))) ")" ) "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_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 "(" (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set "(" (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "y")) ")" ) ")" ) ")" )))) ")" )) ; theorem :: BCIIDEAL:48 (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCK-algebra":::) "holds" (Bool "(" (Bool "(" "for" (Set (Var "I")) "being" ($#m2_bcialg_1 :::"Ideal"::: ) "of" (Set (Var "X")) "holds" (Bool (Set (Var "I")) "is" ($#v3_bciideal :::"commutative"::: ) ($#m2_bcialg_1 :::"Ideal"::: ) "of" (Set (Var "X"))) ")" ) "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 (Var "x")) ($#r1_hidden :::"="::: ) (Set (Set (Var "y")) ($#k1_bcialg_1 :::"\"::: ) (Set "(" (Set (Var "y")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "x")) ")" )))) ")" )) ; theorem :: BCIIDEAL:49 (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCK-algebra":::) "st" (Bool (Bool "(" "for" (Set (Var "I")) "being" ($#m2_bcialg_1 :::"Ideal"::: ) "of" (Set (Var "X")) "holds" (Bool (Set (Var "I")) "is" ($#v3_bciideal :::"commutative"::: ) ($#m2_bcialg_1 :::"Ideal"::: ) "of" (Set (Var "X"))) ")" )) "holds" (Bool "(" (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Var "x"))) "iff" (Bool (Set (Set (Var "y")) ($#k1_bcialg_1 :::"\"::: ) (Set "(" (Set (Var "y")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "x")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "X")))) ")" ) ")" ) & (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 (Var "x")))) "holds" (Bool (Set (Set (Var "y")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Var "y"))) ")" ) & (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "y")) ($#r1_bcialg_1 :::"<="::: ) (Set (Var "a")))) "holds" (Bool (Set (Set "(" (Set (Var "a")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "x")) ")" ) ($#k1_bcialg_1 :::"\"::: ) (Set "(" (Set (Var "a")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "y")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "y")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "x")))) ")" ) & (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set "(" (Set (Var "y")) ($#k1_bcialg_1 :::"\"::: ) (Set "(" (Set (Var "y")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "x")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "y")))) & (Bool (Set (Set "(" (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "y")) ")" ) ($#k1_bcialg_1 :::"\"::: ) (Set "(" (Set "(" (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "y")) ")" ) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "x")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "y")))) ")" ) ")" ) & (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "x")) ($#r1_bcialg_1 :::"<="::: ) (Set (Var "a")))) "holds" (Bool (Set (Set "(" (Set (Var "a")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "y")) ")" ) ($#k1_bcialg_1 :::"\"::: ) (Set "(" (Set "(" (Set (Var "a")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "y")) ")" ) ($#k1_bcialg_1 :::"\"::: ) (Set "(" (Set (Var "a")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "x")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "y")) ")" ) ($#k1_bcialg_1 :::"\"::: ) (Set "(" (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "y")) ")" ))) ")" ) ")" )) ; begin definitionlet "X" be ($#l2_bcialg_1 :::"BCK-algebra":::); mode :::"implicative-ideal"::: "of" "X" -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" "X" means :: BCIIDEAL:def 7 (Bool "(" (Bool (Set ($#k4_struct_0 :::"0."::: ) "X") ($#r2_hidden :::"in"::: ) it) & (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" "X" "st" (Bool (Bool (Set (Set "(" (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set "(" (Set (Var "y")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "x")) ")" ) ")" ) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "z"))) ($#r2_hidden :::"in"::: ) it) & (Bool (Set (Var "z")) ($#r2_hidden :::"in"::: ) it)) "holds" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) it) ")" ) ")" ); end; :: deftheorem defines :::"implicative-ideal"::: BCIIDEAL:def 7 : (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCK-algebra":::) (Bool "for" (Set (Var "b2")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "b2")) "is" ($#m3_bciideal :::"implicative-ideal"::: ) "of" (Set (Var "X"))) "iff" (Bool "(" (Bool (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "X"))) ($#r2_hidden :::"in"::: ) (Set (Var "b2"))) & (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Set "(" (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set "(" (Set (Var "y")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "x")) ")" ) ")" ) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "z"))) ($#r2_hidden :::"in"::: ) (Set (Var "b2"))) & (Bool (Set (Var "z")) ($#r2_hidden :::"in"::: ) (Set (Var "b2")))) "holds" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "b2"))) ")" ) ")" ) ")" ))); theorem :: BCIIDEAL:50 (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCK-algebra":::) (Bool "for" (Set (Var "I")) "being" ($#m2_bcialg_1 :::"Ideal"::: ) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "I")) "is" ($#m3_bciideal :::"implicative-ideal"::: ) "of" (Set (Var "X"))) "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 "(" (Set (Var "y")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "x")) ")" )) ($#r2_hidden :::"in"::: ) (Set (Var "I")))) "holds" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "I")))) ")" ))) ; definitionlet "X" be ($#l2_bcialg_1 :::"BCK-algebra":::); mode :::"positive-implicative-ideal"::: "of" "X" -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" "X" means :: BCIIDEAL:def 8 (Bool "(" (Bool (Set ($#k4_struct_0 :::"0."::: ) "X") ($#r2_hidden :::"in"::: ) it) & (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" "X" "st" (Bool (Bool (Set (Set "(" (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "y")) ")" ) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "z"))) ($#r2_hidden :::"in"::: ) it) & (Bool (Set (Set (Var "y")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "z"))) ($#r2_hidden :::"in"::: ) it)) "holds" (Bool (Set (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "z"))) ($#r2_hidden :::"in"::: ) it) ")" ) ")" ); end; :: deftheorem defines :::"positive-implicative-ideal"::: BCIIDEAL:def 8 : (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCK-algebra":::) (Bool "for" (Set (Var "b2")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "b2")) "is" ($#m4_bciideal :::"positive-implicative-ideal"::: ) "of" (Set (Var "X"))) "iff" (Bool "(" (Bool (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "X"))) ($#r2_hidden :::"in"::: ) (Set (Var "b2"))) & (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Set "(" (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "y")) ")" ) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "z"))) ($#r2_hidden :::"in"::: ) (Set (Var "b2"))) & (Bool (Set (Set (Var "y")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "z"))) ($#r2_hidden :::"in"::: ) (Set (Var "b2")))) "holds" (Bool (Set (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "z"))) ($#r2_hidden :::"in"::: ) (Set (Var "b2"))) ")" ) ")" ) ")" ))); theorem :: BCIIDEAL:51 (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCK-algebra":::) (Bool "for" (Set (Var "I")) "being" ($#m2_bcialg_1 :::"Ideal"::: ) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "I")) "is" ($#m4_bciideal :::"positive-implicative-ideal"::: ) "of" (Set (Var "X"))) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Set "(" (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "y")) ")" ) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "y"))) ($#r2_hidden :::"in"::: ) (Set (Var "I")))) "holds" (Bool (Set (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "y"))) ($#r2_hidden :::"in"::: ) (Set (Var "I")))) ")" ))) ; theorem :: BCIIDEAL:52 (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCK-algebra":::) (Bool "for" (Set (Var "I")) "being" ($#m2_bcialg_1 :::"Ideal"::: ) "of" (Set (Var "X")) "st" (Bool (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Set "(" (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "y")) ")" ) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "z"))) ($#r2_hidden :::"in"::: ) (Set (Var "I"))) & (Bool (Set (Set (Var "y")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "z"))) ($#r2_hidden :::"in"::: ) (Set (Var "I")))) "holds" (Bool (Set (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "z"))) ($#r2_hidden :::"in"::: ) (Set (Var "I"))) ")" )) "holds" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Set "(" (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "y")) ")" ) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "z"))) ($#r2_hidden :::"in"::: ) (Set (Var "I")))) "holds" (Bool (Set (Set "(" (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "z")) ")" ) ($#k1_bcialg_1 :::"\"::: ) (Set "(" (Set (Var "y")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "z")) ")" )) ($#r2_hidden :::"in"::: ) (Set (Var "I")))))) ; theorem :: BCIIDEAL:53 (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCK-algebra":::) (Bool "for" (Set (Var "I")) "being" ($#m2_bcialg_1 :::"Ideal"::: ) "of" (Set (Var "X")) "st" (Bool (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Set "(" (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "y")) ")" ) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "z"))) ($#r2_hidden :::"in"::: ) (Set (Var "I")))) "holds" (Bool (Set (Set "(" (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "z")) ")" ) ($#k1_bcialg_1 :::"\"::: ) (Set "(" (Set (Var "y")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "z")) ")" )) ($#r2_hidden :::"in"::: ) (Set (Var "I"))) ")" )) "holds" (Bool (Set (Var "I")) "is" ($#m4_bciideal :::"positive-implicative-ideal"::: ) "of" (Set (Var "X"))))) ; theorem :: BCIIDEAL:54 (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCK-algebra":::) (Bool "for" (Set (Var "I")) "being" ($#m2_bcialg_1 :::"Ideal"::: ) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "I")) "is" ($#m4_bciideal :::"positive-implicative-ideal"::: ) "of" (Set (Var "X"))) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Set "(" (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "y")) ")" ) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "z"))) ($#r2_hidden :::"in"::: ) (Set (Var "I"))) & (Bool (Set (Set (Var "y")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "z"))) ($#r2_hidden :::"in"::: ) (Set (Var "I")))) "holds" (Bool (Set (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "z"))) ($#r2_hidden :::"in"::: ) (Set (Var "I")))) ")" ))) ; theorem :: BCIIDEAL:55 (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCK-algebra":::) (Bool "for" (Set (Var "I")) "being" ($#m2_bcialg_1 :::"Ideal"::: ) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "I")) "is" ($#m4_bciideal :::"positive-implicative-ideal"::: ) "of" (Set (Var "X"))) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Set "(" (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "y")) ")" ) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "z"))) ($#r2_hidden :::"in"::: ) (Set (Var "I")))) "holds" (Bool (Set (Set "(" (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "z")) ")" ) ($#k1_bcialg_1 :::"\"::: ) (Set "(" (Set (Var "y")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "z")) ")" )) ($#r2_hidden :::"in"::: ) (Set (Var "I")))) ")" ))) ; theorem :: BCIIDEAL:56 (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCK-algebra":::) (Bool "for" (Set (Var "I")) "," (Set (Var "A")) "being" ($#m2_bcialg_1 :::"Ideal"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "I")) ($#r1_tarski :::"c="::: ) (Set (Var "A"))) & (Bool (Set (Var "I")) "is" ($#m4_bciideal :::"positive-implicative-ideal"::: ) "of" (Set (Var "X")))) "holds" (Bool (Set (Var "A")) "is" ($#m4_bciideal :::"positive-implicative-ideal"::: ) "of" (Set (Var "X"))))) ; theorem :: BCIIDEAL:57 (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCK-algebra":::) (Bool "for" (Set (Var "I")) "being" ($#m2_bcialg_1 :::"Ideal"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "I")) "is" ($#m3_bciideal :::"implicative-ideal"::: ) "of" (Set (Var "X")))) "holds" (Bool "(" (Bool (Set (Var "I")) "is" ($#v3_bciideal :::"commutative"::: ) ($#m2_bcialg_1 :::"Ideal"::: ) "of" (Set (Var "X"))) & (Bool (Set (Var "I")) "is" ($#m4_bciideal :::"positive-implicative-ideal"::: ) "of" (Set (Var "X"))) ")" ))) ;