:: FILTER_1  semantic presentation begin  



























































































theorem :: FILTER_1:1 (Bool  "for" (Set (Var "L")) "being"   ($#l3_lattices :::"Lattice":::)  (Bool  "for" (Set (Var "F1")) "," (Set (Var "F2")) "being"   ($#m1_subset_1 :::"Filter":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set (Var "F1"))  ($#k9_subset_1 :::"/\"::: )  (Set (Var "F2"))) "is"   ($#m1_subset_1 :::"Filter":::) "of" (Set (Var "L"))))) ; 
 
theorem :: FILTER_1:2 (Bool  "for" (Set (Var "L")) "being"   ($#l3_lattices :::"Lattice":::)  (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L"))  "st" (Bool (Bool (Set  ($#k2_filter_0 :::"<."::: ) (Set (Var "p")) ($#k2_filter_0 :::".)"::: ) )  ($#r1_hidden :::"="::: )  (Set  ($#k2_filter_0 :::"<."::: ) (Set (Var "q")) ($#k2_filter_0 :::".)"::: ) ))) "holds"  (Bool (Set (Var "p"))  ($#r1_hidden :::"="::: )  (Set (Var "q"))))) ; 
 definitionlet "L" be   ($#l3_lattices :::"Lattice":::); let "F1", "F2" be   ($#m1_subset_1 :::"Filter":::) "of" (Set (Const "L")); :: original: :::"/\"::: redefine func "F1" :::"/\"::: "F2" ->   ($#m1_subset_1 :::"Filter":::) "of" "L"; end; definitionlet "D" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  ; let "R" be   ($#m1_hidden :::"Relation":::); mode  :::"UnOp":::  "of" "D" "," "R" ->   ($#m1_subset_1 :::"UnOp":::) "of" "D" means :: FILTER_1:def 1 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" "D"  "st" (Bool (Bool (Set  ($#k1_domain_1 :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k1_domain_1 :::"]"::: ) )  ($#r2_hidden :::"in"::: )  "R")) "holds"  (Bool (Set  ($#k1_domain_1 :::"["::: ) (Set  "(" it  ($#k3_funct_2 :::"."::: )  (Set (Var "x")) ")" ) "," (Set  "(" it  ($#k3_funct_2 :::"."::: )  (Set (Var "y")) ")" ) ($#k1_domain_1 :::"]"::: ) )  ($#r2_hidden :::"in"::: )  "R")); mode  :::"BinOp":::  "of" "D" "," "R" ->   ($#m1_subset_1 :::"BinOp":::) "of" "D" means :: FILTER_1:def 2 (Bool  "for" (Set (Var "x1")) "," (Set (Var "y1")) "," (Set (Var "x2")) "," (Set (Var "y2")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" "D"  "st" (Bool (Bool (Set  ($#k1_domain_1 :::"["::: ) (Set (Var "x1")) "," (Set (Var "y1")) ($#k1_domain_1 :::"]"::: ) )  ($#r2_hidden :::"in"::: )  "R") & (Bool (Set  ($#k1_domain_1 :::"["::: ) (Set (Var "x2")) "," (Set (Var "y2")) ($#k1_domain_1 :::"]"::: ) )  ($#r2_hidden :::"in"::: )  "R")) "holds"  (Bool (Set  ($#k1_domain_1 :::"["::: ) (Set  "(" it  ($#k5_binop_1 :::"."::: )   "(" (Set (Var "x1")) "," (Set (Var "x2")) ")"  ")" ) "," (Set  "(" it  ($#k5_binop_1 :::"."::: )   "(" (Set (Var "y1")) "," (Set (Var "y2")) ")"  ")" ) ($#k1_domain_1 :::"]"::: ) )  ($#r2_hidden :::"in"::: )  "R")); end; 












:: deftheorem    defines :::"UnOp"::: FILTER_1:def 1 :  (Bool  "for" (Set (Var "D")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "R")) "being"   ($#m1_hidden :::"Relation":::)  (Bool  "for" (Set (Var "b3")) "being"   ($#m1_subset_1 :::"UnOp":::) "of" (Set (Var "D")) "holds"   (Bool  "("  (Bool (Set (Var "b3")) "is"    ($#m1_filter_1 :::"UnOp"::: )   "of" (Set (Var "D")) "," (Set (Var "R"))) "iff" (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "D"))  "st" (Bool (Bool (Set  ($#k1_domain_1 :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k1_domain_1 :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set (Var "R")))) "holds"  (Bool (Set  ($#k1_domain_1 :::"["::: ) (Set  "(" (Set (Var "b3"))  ($#k3_funct_2 :::"."::: )  (Set (Var "x")) ")" ) "," (Set  "(" (Set (Var "b3"))  ($#k3_funct_2 :::"."::: )  (Set (Var "y")) ")" ) ($#k1_domain_1 :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set (Var "R"))))  ")" )))); 
 
:: deftheorem    defines :::"BinOp"::: FILTER_1:def 2 :  (Bool  "for" (Set (Var "D")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "R")) "being"   ($#m1_hidden :::"Relation":::)  (Bool  "for" (Set (Var "b3")) "being"   ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "D")) "holds"   (Bool  "("  (Bool (Set (Var "b3")) "is"    ($#m2_filter_1 :::"BinOp"::: )   "of" (Set (Var "D")) "," (Set (Var "R"))) "iff" (Bool  "for" (Set (Var "x1")) "," (Set (Var "y1")) "," (Set (Var "x2")) "," (Set (Var "y2")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "D"))  "st" (Bool (Bool (Set  ($#k1_domain_1 :::"["::: ) (Set (Var "x1")) "," (Set (Var "y1")) ($#k1_domain_1 :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set (Var "R"))) & (Bool (Set  ($#k1_domain_1 :::"["::: ) (Set (Var "x2")) "," (Set (Var "y2")) ($#k1_domain_1 :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set (Var "R")))) "holds"  (Bool (Set  ($#k1_domain_1 :::"["::: ) (Set  "(" (Set (Var "b3"))  ($#k5_binop_1 :::"."::: )   "(" (Set (Var "x1")) "," (Set (Var "x2")) ")"  ")" ) "," (Set  "(" (Set (Var "b3"))  ($#k5_binop_1 :::"."::: )   "(" (Set (Var "y1")) "," (Set (Var "y2")) ")"  ")" ) ($#k1_domain_1 :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set (Var "R"))))  ")" )))); 
 



definitionlet "D" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  ; let "R" be   ($#m1_subset_1 :::"Equivalence_Relation":::) "of" (Set (Const "D")); mode UnOp of "R" is    ($#m1_filter_1 :::"UnOp"::: )   "of" "D" "," "R"; mode BinOp of "R" is    ($#m2_filter_1 :::"BinOp"::: )   "of" "D" "," "R"; end; definitionlet "D" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  ; let "R" be   ($#m1_subset_1 :::"Equivalence_Relation":::) "of" (Set (Const "D")); let "u" be   ($#m1_subset_1 :::"UnOp":::) "of" (Set (Const "D")); assume 
(Bool (Set (Const "u")) "is"    ($#m1_filter_1 :::"UnOp"::: )   "of" (Set (Const "D")) "," (Set (Const "R")))
 ; func "u" :::"/\/"::: "R" ->   ($#m1_subset_1 :::"UnOp":::) "of" (Set  "("  ($#k8_eqrel_1 :::"Class"::: )  "R" ")" ) means :: FILTER_1:def 3 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k8_eqrel_1 :::"Class"::: )  "R")) & (Bool (Set (Var "y"))  ($#r2_hidden :::"in"::: )  (Set (Var "x")))) "holds"  (Bool (Set it  ($#k1_funct_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_eqrel_1 :::"Class"::: )   "(" "R" "," (Set  "(" "u"  ($#k1_funct_1 :::"."::: )  (Set (Var "y")) ")" ) ")" ))); end; 








:: deftheorem    defines :::"/\/"::: FILTER_1:def 3 :  (Bool  "for" (Set (Var "D")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "R")) "being"   ($#m1_subset_1 :::"Equivalence_Relation":::) "of" (Set (Var "D"))  (Bool  "for" (Set (Var "u")) "being"   ($#m1_subset_1 :::"UnOp":::) "of" (Set (Var "D"))  "st" (Bool (Bool (Set (Var "u")) "is"    ($#m1_filter_1 :::"UnOp"::: )   "of" (Set (Var "D")) "," (Set (Var "R")))) "holds"  (Bool  "for" (Set (Var "b4")) "being"   ($#m1_subset_1 :::"UnOp":::) "of" (Set  "("  ($#k8_eqrel_1 :::"Class"::: )  (Set (Var "R")) ")" ) "holds"   (Bool  "("  (Bool (Set (Var "b4"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "u"))  ($#k2_filter_1 :::"/\/"::: )  (Set (Var "R")))) "iff" (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k8_eqrel_1 :::"Class"::: )  (Set (Var "R")))) & (Bool (Set (Var "y"))  ($#r2_hidden :::"in"::: )  (Set (Var "x")))) "holds"  (Bool (Set (Set (Var "b4"))  ($#k1_funct_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_eqrel_1 :::"Class"::: )   "(" (Set (Var "R")) "," (Set  "(" (Set (Var "u"))  ($#k1_funct_1 :::"."::: )  (Set (Var "y")) ")" ) ")" )))  ")" ))))); 
 definitionlet "D" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  ; let "R" be   ($#m1_subset_1 :::"Equivalence_Relation":::) "of" (Set (Const "D")); let "b" be   ($#m1_subset_1 :::"BinOp":::) "of" (Set (Const "D")); assume 
(Bool (Set (Const "b")) "is"    ($#m2_filter_1 :::"BinOp"::: )   "of" (Set (Const "D")) "," (Set (Const "R")))
 ; func "b" :::"/\/"::: "R" ->   ($#m1_subset_1 :::"BinOp":::) "of" (Set  "("  ($#k8_eqrel_1 :::"Class"::: )  "R" ")" ) means :: FILTER_1:def 4 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "x1")) "," (Set (Var "y1")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k8_eqrel_1 :::"Class"::: )  "R")) & (Bool (Set (Var "y"))  ($#r2_hidden :::"in"::: )  (Set   ($#k8_eqrel_1 :::"Class"::: )  "R")) & (Bool (Set (Var "x1"))  ($#r2_hidden :::"in"::: )  (Set (Var "x"))) & (Bool (Set (Var "y1"))  ($#r2_hidden :::"in"::: )  (Set (Var "y")))) "holds"  (Bool (Set it  ($#k1_binop_1 :::"."::: )   "(" (Set (Var "x")) "," (Set (Var "y")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k6_eqrel_1 :::"Class"::: )   "(" "R" "," (Set  "(" "b"  ($#k1_binop_1 :::"."::: )   "(" (Set (Var "x1")) "," (Set (Var "y1")) ")"  ")" ) ")" ))); end; 








:: deftheorem    defines :::"/\/"::: FILTER_1:def 4 :  (Bool  "for" (Set (Var "D")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "R")) "being"   ($#m1_subset_1 :::"Equivalence_Relation":::) "of" (Set (Var "D"))  (Bool  "for" (Set (Var "b")) "being"   ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "D"))  "st" (Bool (Bool (Set (Var "b")) "is"    ($#m2_filter_1 :::"BinOp"::: )   "of" (Set (Var "D")) "," (Set (Var "R")))) "holds"  (Bool  "for" (Set (Var "b4")) "being"   ($#m1_subset_1 :::"BinOp":::) "of" (Set  "("  ($#k8_eqrel_1 :::"Class"::: )  (Set (Var "R")) ")" ) "holds"   (Bool  "("  (Bool (Set (Var "b4"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "b"))  ($#k3_filter_1 :::"/\/"::: )  (Set (Var "R")))) "iff" (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "x1")) "," (Set (Var "y1")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k8_eqrel_1 :::"Class"::: )  (Set (Var "R")))) & (Bool (Set (Var "y"))  ($#r2_hidden :::"in"::: )  (Set   ($#k8_eqrel_1 :::"Class"::: )  (Set (Var "R")))) & (Bool (Set (Var "x1"))  ($#r2_hidden :::"in"::: )  (Set (Var "x"))) & (Bool (Set (Var "y1"))  ($#r2_hidden :::"in"::: )  (Set (Var "y")))) "holds"  (Bool (Set (Set (Var "b4"))  ($#k1_binop_1 :::"."::: )   "(" (Set (Var "x")) "," (Set (Var "y")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k6_eqrel_1 :::"Class"::: )   "(" (Set (Var "R")) "," (Set  "(" (Set (Var "b"))  ($#k1_binop_1 :::"."::: )   "(" (Set (Var "x1")) "," (Set (Var "y1")) ")"  ")" ) ")" )))  ")" ))))); 
 
theorem :: FILTER_1:3 (Bool  "for" (Set (Var "D")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "RD")) "being"   ($#m1_subset_1 :::"Equivalence_Relation":::) "of" (Set (Var "D"))  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "D"))  (Bool  "for" (Set (Var "F")) "being"    ($#m2_filter_1 :::"BinOp"::: )   "of" (Set (Var "D")) "," (Set (Var "RD")) "holds"  (Bool (Set (Set  "(" (Set (Var "F"))  ($#k3_filter_1 :::"/\/"::: )  (Set (Var "RD")) ")" )  ($#k1_binop_1 :::"."::: )   "(" (Set  "("  ($#k6_eqrel_1 :::"Class"::: )   "(" (Set (Var "RD")) "," (Set (Var "a")) ")"  ")" ) "," (Set  "("  ($#k6_eqrel_1 :::"Class"::: )   "(" (Set (Var "RD")) "," (Set (Var "b")) ")"  ")" ) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k6_eqrel_1 :::"Class"::: )   "(" (Set (Var "RD")) "," (Set  "(" (Set (Var "F"))  ($#k5_binop_1 :::"."::: )   "(" (Set (Var "a")) "," (Set (Var "b")) ")"  ")" ) ")" )))))) ; 
 scheme  :: FILTER_1:sch 1 SchAux1{ F1() ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  , F2() ->   ($#m1_subset_1 :::"Equivalence_Relation":::) "of" (Set F1 "("  ")" ), P1[   ($#m1_hidden :::"set"::: )  ] } : 
(Bool  "for" (Set (Var "x")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k8_eqrel_1 :::"Class"::: )  (Set F2 "("  ")" )) "holds"  (Bool P1[(Set (Var "x"))]))
 provided
(Bool  "for" (Set (Var "x")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set F1 "("  ")" ) "holds"  (Bool P1[(Set   ($#k9_eqrel_1 :::"EqClass"::: )   "(" (Set F2 "("  ")" ) "," (Set (Var "x")) ")" )]))
 proof 


end; scheme  :: FILTER_1:sch 2 SchAux2{ F1() ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  , F2() ->   ($#m1_subset_1 :::"Equivalence_Relation":::) "of" (Set F1 "("  ")" ), P1[   ($#m1_hidden :::"set"::: )   ","    ($#m1_hidden :::"set"::: )  ] } : 
(Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k8_eqrel_1 :::"Class"::: )  (Set F2 "("  ")" )) "holds"  (Bool P1[(Set (Var "x")) "," (Set (Var "y"))]))
 provided
(Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set F1 "("  ")" ) "holds"  (Bool P1[(Set   ($#k9_eqrel_1 :::"EqClass"::: )   "(" (Set F2 "("  ")" ) "," (Set (Var "x")) ")" ) "," (Set   ($#k9_eqrel_1 :::"EqClass"::: )   "(" (Set F2 "("  ")" ) "," (Set (Var "y")) ")" )]))
 proof 


end; scheme  :: FILTER_1:sch 3 SchAux3{ F1() ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  , F2() ->   ($#m1_subset_1 :::"Equivalence_Relation":::) "of" (Set F1 "("  ")" ), P1[   ($#m1_hidden :::"set"::: )   ","    ($#m1_hidden :::"set"::: )   ","    ($#m1_hidden :::"set"::: )  ] } : 
(Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k8_eqrel_1 :::"Class"::: )  (Set F2 "("  ")" )) "holds"  (Bool P1[(Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z"))]))
 provided
(Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set F1 "("  ")" ) "holds"  (Bool P1[(Set   ($#k9_eqrel_1 :::"EqClass"::: )   "(" (Set F2 "("  ")" ) "," (Set (Var "x")) ")" ) "," (Set   ($#k9_eqrel_1 :::"EqClass"::: )   "(" (Set F2 "("  ")" ) "," (Set (Var "y")) ")" ) "," (Set   ($#k9_eqrel_1 :::"EqClass"::: )   "(" (Set F2 "("  ")" ) "," (Set (Var "z")) ")" )]))
 proof 


end; 
theorem :: FILTER_1:4 (Bool  "for" (Set (Var "D")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "RD")) "being"   ($#m1_subset_1 :::"Equivalence_Relation":::) "of" (Set (Var "D"))  (Bool  "for" (Set (Var "F")) "being"    ($#m2_filter_1 :::"BinOp"::: )   "of" (Set (Var "D")) "," (Set (Var "RD"))  "st" (Bool (Bool (Set (Var "F")) "is"   ($#v1_binop_1 :::"commutative"::: )  )) "holds"  (Bool (Set (Set (Var "F"))  ($#k3_filter_1 :::"/\/"::: )  (Set (Var "RD"))) "is"   ($#v1_binop_1 :::"commutative"::: )  )))) ; 
 
theorem :: FILTER_1:5 (Bool  "for" (Set (Var "D")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "RD")) "being"   ($#m1_subset_1 :::"Equivalence_Relation":::) "of" (Set (Var "D"))  (Bool  "for" (Set (Var "F")) "being"    ($#m2_filter_1 :::"BinOp"::: )   "of" (Set (Var "D")) "," (Set (Var "RD"))  "st" (Bool (Bool (Set (Var "F")) "is"   ($#v2_binop_1 :::"associative"::: )  )) "holds"  (Bool (Set (Set (Var "F"))  ($#k3_filter_1 :::"/\/"::: )  (Set (Var "RD"))) "is"   ($#v2_binop_1 :::"associative"::: )  )))) ; 
 
theorem :: FILTER_1:6 (Bool  "for" (Set (Var "D")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "RD")) "being"   ($#m1_subset_1 :::"Equivalence_Relation":::) "of" (Set (Var "D"))  (Bool  "for" (Set (Var "d")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "D"))  (Bool  "for" (Set (Var "F")) "being"    ($#m2_filter_1 :::"BinOp"::: )   "of" (Set (Var "D")) "," (Set (Var "RD"))  "st" (Bool (Bool (Set (Var "d"))  ($#r1_binop_1 :::"is_a_left_unity_wrt"::: )  (Set (Var "F")))) "holds"  (Bool (Set   ($#k9_eqrel_1 :::"EqClass"::: )   "(" (Set (Var "RD")) "," (Set (Var "d")) ")" )  ($#r1_binop_1 :::"is_a_left_unity_wrt"::: )  (Set (Set (Var "F"))  ($#k3_filter_1 :::"/\/"::: )  (Set (Var "RD")))))))) ; 
 
theorem :: FILTER_1:7 (Bool  "for" (Set (Var "D")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "RD")) "being"   ($#m1_subset_1 :::"Equivalence_Relation":::) "of" (Set (Var "D"))  (Bool  "for" (Set (Var "d")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "D"))  (Bool  "for" (Set (Var "F")) "being"    ($#m2_filter_1 :::"BinOp"::: )   "of" (Set (Var "D")) "," (Set (Var "RD"))  "st" (Bool (Bool (Set (Var "d"))  ($#r2_binop_1 :::"is_a_right_unity_wrt"::: )  (Set (Var "F")))) "holds"  (Bool (Set   ($#k9_eqrel_1 :::"EqClass"::: )   "(" (Set (Var "RD")) "," (Set (Var "d")) ")" )  ($#r2_binop_1 :::"is_a_right_unity_wrt"::: )  (Set (Set (Var "F"))  ($#k3_filter_1 :::"/\/"::: )  (Set (Var "RD")))))))) ; 
 
theorem :: FILTER_1:8 (Bool  "for" (Set (Var "D")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "RD")) "being"   ($#m1_subset_1 :::"Equivalence_Relation":::) "of" (Set (Var "D"))  (Bool  "for" (Set (Var "d")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "D"))  (Bool  "for" (Set (Var "F")) "being"    ($#m2_filter_1 :::"BinOp"::: )   "of" (Set (Var "D")) "," (Set (Var "RD"))  "st" (Bool (Bool (Set (Var "d"))  ($#r3_binop_1 :::"is_a_unity_wrt"::: )  (Set (Var "F")))) "holds"  (Bool (Set   ($#k9_eqrel_1 :::"EqClass"::: )   "(" (Set (Var "RD")) "," (Set (Var "d")) ")" )  ($#r3_binop_1 :::"is_a_unity_wrt"::: )  (Set (Set (Var "F"))  ($#k3_filter_1 :::"/\/"::: )  (Set (Var "RD")))))))) ; 
 
theorem :: FILTER_1:9 (Bool  "for" (Set (Var "D")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "RD")) "being"   ($#m1_subset_1 :::"Equivalence_Relation":::) "of" (Set (Var "D"))  (Bool  "for" (Set (Var "F")) "," (Set (Var "G")) "being"    ($#m2_filter_1 :::"BinOp"::: )   "of" (Set (Var "D")) "," (Set (Var "RD"))  "st" (Bool (Bool (Set (Var "F"))  ($#r4_binop_1 :::"is_left_distributive_wrt"::: )  (Set (Var "G")))) "holds"  (Bool (Set (Set (Var "F"))  ($#k3_filter_1 :::"/\/"::: )  (Set (Var "RD")))  ($#r4_binop_1 :::"is_left_distributive_wrt"::: )  (Set (Set (Var "G"))  ($#k3_filter_1 :::"/\/"::: )  (Set (Var "RD"))))))) ; 
 
theorem :: FILTER_1:10 (Bool  "for" (Set (Var "D")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "RD")) "being"   ($#m1_subset_1 :::"Equivalence_Relation":::) "of" (Set (Var "D"))  (Bool  "for" (Set (Var "F")) "," (Set (Var "G")) "being"    ($#m2_filter_1 :::"BinOp"::: )   "of" (Set (Var "D")) "," (Set (Var "RD"))  "st" (Bool (Bool (Set (Var "F"))  ($#r5_binop_1 :::"is_right_distributive_wrt"::: )  (Set (Var "G")))) "holds"  (Bool (Set (Set (Var "F"))  ($#k3_filter_1 :::"/\/"::: )  (Set (Var "RD")))  ($#r5_binop_1 :::"is_right_distributive_wrt"::: )  (Set (Set (Var "G"))  ($#k3_filter_1 :::"/\/"::: )  (Set (Var "RD"))))))) ; 
 
theorem :: FILTER_1:11 (Bool  "for" (Set (Var "D")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "RD")) "being"   ($#m1_subset_1 :::"Equivalence_Relation":::) "of" (Set (Var "D"))  (Bool  "for" (Set (Var "F")) "," (Set (Var "G")) "being"    ($#m2_filter_1 :::"BinOp"::: )   "of" (Set (Var "D")) "," (Set (Var "RD"))  "st" (Bool (Bool (Set (Var "F"))  ($#r6_binop_1 :::"is_distributive_wrt"::: )  (Set (Var "G")))) "holds"  (Bool (Set (Set (Var "F"))  ($#k3_filter_1 :::"/\/"::: )  (Set (Var "RD")))  ($#r6_binop_1 :::"is_distributive_wrt"::: )  (Set (Set (Var "G"))  ($#k3_filter_1 :::"/\/"::: )  (Set (Var "RD"))))))) ; 
 
theorem :: FILTER_1:12 (Bool  "for" (Set (Var "D")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "RD")) "being"   ($#m1_subset_1 :::"Equivalence_Relation":::) "of" (Set (Var "D"))  (Bool  "for" (Set (Var "F")) "," (Set (Var "G")) "being"    ($#m2_filter_1 :::"BinOp"::: )   "of" (Set (Var "D")) "," (Set (Var "RD"))  "st" (Bool (Bool (Set (Var "F"))  ($#r1_lattice2 :::"absorbs"::: )  (Set (Var "G")))) "holds"  (Bool (Set (Set (Var "F"))  ($#k3_filter_1 :::"/\/"::: )  (Set (Var "RD")))  ($#r1_lattice2 :::"absorbs"::: )  (Set (Set (Var "G"))  ($#k3_filter_1 :::"/\/"::: )  (Set (Var "RD"))))))) ; 
 
theorem :: FILTER_1:13 (Bool  "for" (Set (Var "I")) "being"   ($#l3_lattices :::"I_Lattice":::)  (Bool  "for" (Set (Var "FI")) "being"   ($#m1_subset_1 :::"Filter":::) "of" (Set (Var "I")) "holds"  (Bool (Set  "the"  ($#u2_lattices :::"L_join"::: )  "of" (Set (Var "I"))) "is"    ($#m2_filter_1 :::"BinOp"::: )   "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "I"))) "," (Set   ($#k9_filter_0 :::"equivalence_wrt"::: )  (Set (Var "FI")))))) ; 
 
theorem :: FILTER_1:14 (Bool  "for" (Set (Var "I")) "being"   ($#l3_lattices :::"I_Lattice":::)  (Bool  "for" (Set (Var "FI")) "being"   ($#m1_subset_1 :::"Filter":::) "of" (Set (Var "I")) "holds"  (Bool (Set  "the"  ($#u1_lattices :::"L_meet"::: )  "of" (Set (Var "I"))) "is"    ($#m2_filter_1 :::"BinOp"::: )   "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "I"))) "," (Set   ($#k9_filter_0 :::"equivalence_wrt"::: )  (Set (Var "FI")))))) ; 
 definitionlet "L" be   ($#l3_lattices :::"Lattice":::); let "F" be   ($#m1_subset_1 :::"Filter":::) "of" (Set (Const "L")); assume 
(Bool (Set (Const "L")) "is"   ($#l3_lattices :::"I_Lattice":::))
 ; func "L" :::"/\/"::: "F" ->   ($#v3_lattices :::"strict"::: )    ($#l3_lattices :::"Lattice":::) means :: FILTER_1:def 5 (Bool  "for" (Set (Var "R")) "being"   ($#m1_subset_1 :::"Equivalence_Relation":::) "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "L")  "st" (Bool (Bool (Set (Var "R"))  ($#r1_hidden :::"="::: )  (Set   ($#k8_filter_0 :::"equivalence_wrt"::: )  "F"))) "holds"  (Bool it  ($#r1_hidden :::"="::: )  (Set   ($#g3_lattices :::"LattStr"::: )  "(#"  (Set  "("  ($#k8_eqrel_1 :::"Class"::: )  (Set (Var "R")) ")" ) "," (Set  "(" (Set  "the"  ($#u2_lattices :::"L_join"::: )  "of" "L")  ($#k3_filter_1 :::"/\/"::: )  (Set (Var "R")) ")" ) "," (Set  "(" (Set  "the"  ($#u1_lattices :::"L_meet"::: )  "of" "L")  ($#k3_filter_1 :::"/\/"::: )  (Set (Var "R")) ")" ) "#)" ))); end; 







:: deftheorem    defines :::"/\/"::: FILTER_1:def 5 :  (Bool  "for" (Set (Var "L")) "being"   ($#l3_lattices :::"Lattice":::)  (Bool  "for" (Set (Var "F")) "being"   ($#m1_subset_1 :::"Filter":::) "of" (Set (Var "L"))  "st" (Bool (Bool (Set (Var "L")) "is"   ($#l3_lattices :::"I_Lattice":::))) "holds"  (Bool  "for" (Set (Var "b3")) "being"   ($#v3_lattices :::"strict"::: )    ($#l3_lattices :::"Lattice":::) "holds"   (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "L"))  ($#k4_filter_1 :::"/\/"::: )  (Set (Var "F")))) "iff" (Bool  "for" (Set (Var "R")) "being"   ($#m1_subset_1 :::"Equivalence_Relation":::) "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "L")))  "st" (Bool (Bool (Set (Var "R"))  ($#r1_hidden :::"="::: )  (Set   ($#k8_filter_0 :::"equivalence_wrt"::: )  (Set (Var "F"))))) "holds"  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set   ($#g3_lattices :::"LattStr"::: )  "(#"  (Set  "("  ($#k8_eqrel_1 :::"Class"::: )  (Set (Var "R")) ")" ) "," (Set  "(" (Set  "the"  ($#u2_lattices :::"L_join"::: )  "of" (Set (Var "L")))  ($#k3_filter_1 :::"/\/"::: )  (Set (Var "R")) ")" ) "," (Set  "(" (Set  "the"  ($#u1_lattices :::"L_meet"::: )  "of" (Set (Var "L")))  ($#k3_filter_1 :::"/\/"::: )  (Set (Var "R")) ")" ) "#)" )))  ")" )))); 
 definitionlet "L" be   ($#l3_lattices :::"Lattice":::); let "F" be   ($#m1_subset_1 :::"Filter":::) "of" (Set (Const "L")); let "a" be   ($#m1_subset_1 :::"Element":::) "of" (Set (Const "L")); assume 
(Bool (Set (Const "L")) "is"   ($#l3_lattices :::"I_Lattice":::))
 ; func "a" :::"/\/"::: "F" ->   ($#m1_subset_1 :::"Element":::) "of" (Set  "(" "L"  ($#k4_filter_1 :::"/\/"::: )  "F" ")" ) means :: FILTER_1:def 6 (Bool  "for" (Set (Var "R")) "being"   ($#m1_subset_1 :::"Equivalence_Relation":::) "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "L")  "st" (Bool (Bool (Set (Var "R"))  ($#r1_hidden :::"="::: )  (Set   ($#k8_filter_0 :::"equivalence_wrt"::: )  "F"))) "holds"  (Bool it  ($#r1_hidden :::"="::: )  (Set   ($#k6_eqrel_1 :::"Class"::: )   "(" (Set (Var "R")) "," "a" ")" ))); end; 








:: deftheorem    defines :::"/\/"::: FILTER_1:def 6 :  (Bool  "for" (Set (Var "L")) "being"   ($#l3_lattices :::"Lattice":::)  (Bool  "for" (Set (Var "F")) "being"   ($#m1_subset_1 :::"Filter":::) "of" (Set (Var "L"))  (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L"))  "st" (Bool (Bool (Set (Var "L")) "is"   ($#l3_lattices :::"I_Lattice":::))) "holds"  (Bool  "for" (Set (Var "b4")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set  "(" (Set (Var "L"))  ($#k4_filter_1 :::"/\/"::: )  (Set (Var "F")) ")" ) "holds"   (Bool  "("  (Bool (Set (Var "b4"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k5_filter_1 :::"/\/"::: )  (Set (Var "F")))) "iff" (Bool  "for" (Set (Var "R")) "being"   ($#m1_subset_1 :::"Equivalence_Relation":::) "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "L")))  "st" (Bool (Bool (Set (Var "R"))  ($#r1_hidden :::"="::: )  (Set   ($#k8_filter_0 :::"equivalence_wrt"::: )  (Set (Var "F"))))) "holds"  (Bool (Set (Var "b4"))  ($#r1_hidden :::"="::: )  (Set   ($#k6_eqrel_1 :::"Class"::: )   "(" (Set (Var "R")) "," (Set (Var "a")) ")" )))  ")" ))))); 
 
theorem :: FILTER_1:15 (Bool  "for" (Set (Var "I")) "being"   ($#l3_lattices :::"I_Lattice":::)  (Bool  "for" (Set (Var "FI")) "being"   ($#m1_subset_1 :::"Filter":::) "of" (Set (Var "I"))  (Bool  "for" (Set (Var "i")) "," (Set (Var "j")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "I")) "holds"   (Bool  "("  (Bool (Set (Set  "(" (Set (Var "i"))  ($#k5_filter_1 :::"/\/"::: )  (Set (Var "FI")) ")" )  ($#k3_lattices :::""\/""::: )  (Set  "(" (Set (Var "j"))  ($#k5_filter_1 :::"/\/"::: )  (Set (Var "FI")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "i"))  ($#k3_lattices :::""\/""::: )  (Set (Var "j")) ")" )  ($#k5_filter_1 :::"/\/"::: )  (Set (Var "FI")))) & (Bool (Set (Set  "(" (Set (Var "i"))  ($#k5_filter_1 :::"/\/"::: )  (Set (Var "FI")) ")" )  ($#k4_lattices :::""/\""::: )  (Set  "(" (Set (Var "j"))  ($#k5_filter_1 :::"/\/"::: )  (Set (Var "FI")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "i"))  ($#k4_lattices :::""/\""::: )  (Set (Var "j")) ")" )  ($#k5_filter_1 :::"/\/"::: )  (Set (Var "FI"))))  ")" )))) ; 
 
theorem :: FILTER_1:16 (Bool  "for" (Set (Var "I")) "being"   ($#l3_lattices :::"I_Lattice":::)  (Bool  "for" (Set (Var "FI")) "being"   ($#m1_subset_1 :::"Filter":::) "of" (Set (Var "I"))  (Bool  "for" (Set (Var "i")) "," (Set (Var "j")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "I")) "holds"   (Bool  "("  (Bool (Set (Set (Var "i"))  ($#k5_filter_1 :::"/\/"::: )  (Set (Var "FI")))  ($#r3_lattices :::"[="::: )  (Set (Set (Var "j"))  ($#k5_filter_1 :::"/\/"::: )  (Set (Var "FI")))) "iff" (Bool (Set (Set (Var "i"))  ($#k4_filter_0 :::"=>"::: )  (Set (Var "j")))  ($#r2_hidden :::"in"::: )  (Set (Var "FI")))  ")" )))) ; 
 
theorem :: FILTER_1:17 (Bool  "for" (Set (Var "I")) "being"   ($#l3_lattices :::"I_Lattice":::)  (Bool  "for" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "k")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "I")) "holds"  (Bool (Set (Set  "(" (Set (Var "i"))  ($#k4_lattices :::""/\""::: )  (Set (Var "j")) ")" )  ($#k4_filter_0 :::"=>"::: )  (Set (Var "k")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "i"))  ($#k4_filter_0 :::"=>"::: )  (Set  "(" (Set (Var "j"))  ($#k4_filter_0 :::"=>"::: )  (Set (Var "k")) ")" ))))) ; 
 
theorem :: FILTER_1:18 (Bool  "for" (Set (Var "I")) "being"   ($#l3_lattices :::"I_Lattice":::)  (Bool  "for" (Set (Var "FI")) "being"   ($#m1_subset_1 :::"Filter":::) "of" (Set (Var "I"))  "st" (Bool (Bool (Set (Var "I")) "is"   ($#v13_lattices :::"lower-bounded"::: )  )) "holds"  (Bool  "("  (Bool (Set (Set (Var "I"))  ($#k4_filter_1 :::"/\/"::: )  (Set (Var "FI"))) "is"   ($#l3_lattices :::"0_Lattice":::)) & (Bool (Set   ($#k5_lattices :::"Bottom"::: )  (Set  "(" (Set (Var "I"))  ($#k4_filter_1 :::"/\/"::: )  (Set (Var "FI")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k5_lattices :::"Bottom"::: )  (Set (Var "I")) ")" )  ($#k5_filter_1 :::"/\/"::: )  (Set (Var "FI"))))  ")" ))) ; 
 
theorem :: FILTER_1:19 (Bool  "for" (Set (Var "I")) "being"   ($#l3_lattices :::"I_Lattice":::)  (Bool  "for" (Set (Var "FI")) "being"   ($#m1_subset_1 :::"Filter":::) "of" (Set (Var "I")) "holds"   (Bool  "("  (Bool (Set (Set (Var "I"))  ($#k4_filter_1 :::"/\/"::: )  (Set (Var "FI"))) "is"   ($#l3_lattices :::"1_Lattice":::)) & (Bool (Set   ($#k6_lattices :::"Top"::: )  (Set  "(" (Set (Var "I"))  ($#k4_filter_1 :::"/\/"::: )  (Set (Var "FI")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k6_lattices :::"Top"::: )  (Set (Var "I")) ")" )  ($#k5_filter_1 :::"/\/"::: )  (Set (Var "FI"))))  ")" ))) ; 
 registrationlet "I" be   ($#l3_lattices :::"I_Lattice":::); let "FI" be   ($#m1_subset_1 :::"Filter":::) "of" (Set (Const "I")); 
cluster (Set "I"  ($#k4_filter_1 :::"/\/"::: )  "FI") ->   ($#v3_lattices :::"strict"::: )     ($#v3_filter_0 :::"implicative"::: )   ; 
end; 
theorem :: FILTER_1:20 (Bool  "for" (Set (Var "B")) "being"   ($#l3_lattices :::"B_Lattice":::)  (Bool  "for" (Set (Var "FB")) "being"   ($#m1_subset_1 :::"Filter":::) "of" (Set (Var "B")) "holds"  (Bool (Set (Set (Var "B"))  ($#k4_filter_1 :::"/\/"::: )  (Set (Var "FB"))) "is"   ($#l3_lattices :::"B_Lattice":::)))) ; 
 definitionlet "D1", "D2" be    ($#m1_hidden :::"set"::: )  ; let "f1" be   ($#m1_subset_1 :::"BinOp":::) "of" (Set (Const "D1")); let "f2" be   ($#m1_subset_1 :::"BinOp":::) "of" (Set (Const "D2")); :: original: :::"|:"::: redefine func :::"|:":::"f1" "," "f2":::":|"::: ->   ($#m1_subset_1 :::"BinOp":::) "of" (Set  ($#k2_zfmisc_1 :::"[:"::: ) "D1" "," "D2" ($#k2_zfmisc_1 :::":]"::: ) ); end; 
theorem :: FILTER_1:21 (Bool  "for" (Set (Var "D1")) "," (Set (Var "D2")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "a1")) "," (Set (Var "b1")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "D1"))  (Bool  "for" (Set (Var "a2")) "," (Set (Var "b2")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "D2"))  (Bool  "for" (Set (Var "f1")) "being"   ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "D1"))  (Bool  "for" (Set (Var "f2")) "being"   ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "D2")) "holds"  (Bool (Set (Set  ($#k6_filter_1 :::"|:"::: ) (Set (Var "f1")) "," (Set (Var "f2")) ($#k6_filter_1 :::":|"::: ) )  ($#k5_binop_1 :::"."::: )   "(" (Set  ($#k1_domain_1 :::"["::: ) (Set (Var "a1")) "," (Set (Var "a2")) ($#k1_domain_1 :::"]"::: ) ) "," (Set  ($#k1_domain_1 :::"["::: ) (Set (Var "b1")) "," (Set (Var "b2")) ($#k1_domain_1 :::"]"::: ) ) ")" )  ($#r1_hidden :::"="::: )  (Set  ($#k1_domain_1 :::"["::: ) (Set  "(" (Set (Var "f1"))  ($#k5_binop_1 :::"."::: )   "(" (Set (Var "a1")) "," (Set (Var "b1")) ")"  ")" ) "," (Set  "(" (Set (Var "f2"))  ($#k5_binop_1 :::"."::: )   "(" (Set (Var "a2")) "," (Set (Var "b2")) ")"  ")" ) ($#k1_domain_1 :::"]"::: ) ))))))) ; 
 scheme  :: FILTER_1:sch 4 AuxCart1{ F1() ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  , F2() ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  , P1[   ($#m1_hidden :::"set"::: )  ] } : 
(Bool  "for" (Set (Var "d")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set F1 "("  ")" ) "," (Set F2 "("  ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) "holds"  (Bool P1[(Set (Var "d"))]))
 provided
(Bool  "for" (Set (Var "d1")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set F1 "("  ")" )  (Bool  "for" (Set (Var "d2")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set F2 "("  ")" ) "holds"  (Bool P1[(Set  ($#k1_domain_1 :::"["::: ) (Set (Var "d1")) "," (Set (Var "d2")) ($#k1_domain_1 :::"]"::: ) )])))
 proof 


end; scheme  :: FILTER_1:sch 5 AuxCart2{ F1() ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  , F2() ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  , P1[   ($#m1_hidden :::"set"::: )   ","    ($#m1_hidden :::"set"::: )  ] } : 
(Bool  "for" (Set (Var "d")) "," (Set (Var "d9")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set F1 "("  ")" ) "," (Set F2 "("  ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) "holds"  (Bool P1[(Set (Var "d")) "," (Set (Var "d9"))]))
 provided
(Bool  "for" (Set (Var "d1")) "," (Set (Var "d19")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set F1 "("  ")" )  (Bool  "for" (Set (Var "d2")) "," (Set (Var "d29")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set F2 "("  ")" ) "holds"  (Bool P1[(Set  ($#k1_domain_1 :::"["::: ) (Set (Var "d1")) "," (Set (Var "d2")) ($#k1_domain_1 :::"]"::: ) ) "," (Set  ($#k1_domain_1 :::"["::: ) (Set (Var "d19")) "," (Set (Var "d29")) ($#k1_domain_1 :::"]"::: ) )])))
 proof 


end; scheme  :: FILTER_1:sch 6 AuxCart3{ F1() ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  , F2() ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  , P1[   ($#m1_hidden :::"set"::: )   ","    ($#m1_hidden :::"set"::: )   ","    ($#m1_hidden :::"set"::: )  ] } : 
(Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set F1 "("  ")" ) "," (Set F2 "("  ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) "holds"  (Bool P1[(Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c"))]))
 provided
(Bool  "for" (Set (Var "a1")) "," (Set (Var "b1")) "," (Set (Var "c1")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set F1 "("  ")" )  (Bool  "for" (Set (Var "a2")) "," (Set (Var "b2")) "," (Set (Var "c2")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set F2 "("  ")" ) "holds"  (Bool P1[(Set  ($#k1_domain_1 :::"["::: ) (Set (Var "a1")) "," (Set (Var "a2")) ($#k1_domain_1 :::"]"::: ) ) "," (Set  ($#k1_domain_1 :::"["::: ) (Set (Var "b1")) "," (Set (Var "b2")) ($#k1_domain_1 :::"]"::: ) ) "," (Set  ($#k1_domain_1 :::"["::: ) (Set (Var "c1")) "," (Set (Var "c2")) ($#k1_domain_1 :::"]"::: ) )])))
 proof 


end; 
theorem :: FILTER_1:22 (Bool  "for" (Set (Var "D1")) "," (Set (Var "D2")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "f1")) "being"   ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "D1"))  (Bool  "for" (Set (Var "f2")) "being"   ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "D2")) "holds"   (Bool  "("  (Bool  "("  (Bool (Set (Var "f1")) "is"   ($#v1_binop_1 :::"commutative"::: )  ) & (Bool (Set (Var "f2")) "is"   ($#v1_binop_1 :::"commutative"::: )  )  ")" ) "iff" (Bool (Set  ($#k6_filter_1 :::"|:"::: ) (Set (Var "f1")) "," (Set (Var "f2")) ($#k6_filter_1 :::":|"::: ) ) "is"   ($#v1_binop_1 :::"commutative"::: )  )  ")" )))) ; 
 
theorem :: FILTER_1:23 (Bool  "for" (Set (Var "D1")) "," (Set (Var "D2")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "f1")) "being"   ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "D1"))  (Bool  "for" (Set (Var "f2")) "being"   ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "D2")) "holds"   (Bool  "("  (Bool  "("  (Bool (Set (Var "f1")) "is"   ($#v2_binop_1 :::"associative"::: )  ) & (Bool (Set (Var "f2")) "is"   ($#v2_binop_1 :::"associative"::: )  )  ")" ) "iff" (Bool (Set  ($#k6_filter_1 :::"|:"::: ) (Set (Var "f1")) "," (Set (Var "f2")) ($#k6_filter_1 :::":|"::: ) ) "is"   ($#v2_binop_1 :::"associative"::: )  )  ")" )))) ; 
 
theorem :: FILTER_1:24 (Bool  "for" (Set (Var "D1")) "," (Set (Var "D2")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "a1")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "D1"))  (Bool  "for" (Set (Var "a2")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "D2"))  (Bool  "for" (Set (Var "f1")) "being"   ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "D1"))  (Bool  "for" (Set (Var "f2")) "being"   ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "D2")) "holds"   (Bool  "("  (Bool  "("  (Bool (Set (Var "a1"))  ($#r1_binop_1 :::"is_a_left_unity_wrt"::: )  (Set (Var "f1"))) & (Bool (Set (Var "a2"))  ($#r1_binop_1 :::"is_a_left_unity_wrt"::: )  (Set (Var "f2")))  ")" ) "iff" (Bool (Set  ($#k1_domain_1 :::"["::: ) (Set (Var "a1")) "," (Set (Var "a2")) ($#k1_domain_1 :::"]"::: ) )  ($#r1_binop_1 :::"is_a_left_unity_wrt"::: )  (Set  ($#k6_filter_1 :::"|:"::: ) (Set (Var "f1")) "," (Set (Var "f2")) ($#k6_filter_1 :::":|"::: ) ))  ")" )))))) ; 
 
theorem :: FILTER_1:25 (Bool  "for" (Set (Var "D1")) "," (Set (Var "D2")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "a1")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "D1"))  (Bool  "for" (Set (Var "a2")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "D2"))  (Bool  "for" (Set (Var "f1")) "being"   ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "D1"))  (Bool  "for" (Set (Var "f2")) "being"   ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "D2")) "holds"   (Bool  "("  (Bool  "("  (Bool (Set (Var "a1"))  ($#r2_binop_1 :::"is_a_right_unity_wrt"::: )  (Set (Var "f1"))) & (Bool (Set (Var "a2"))  ($#r2_binop_1 :::"is_a_right_unity_wrt"::: )  (Set (Var "f2")))  ")" ) "iff" (Bool (Set  ($#k1_domain_1 :::"["::: ) (Set (Var "a1")) "," (Set (Var "a2")) ($#k1_domain_1 :::"]"::: ) )  ($#r2_binop_1 :::"is_a_right_unity_wrt"::: )  (Set  ($#k6_filter_1 :::"|:"::: ) (Set (Var "f1")) "," (Set (Var "f2")) ($#k6_filter_1 :::":|"::: ) ))  ")" )))))) ; 
 
theorem :: FILTER_1:26 (Bool  "for" (Set (Var "D1")) "," (Set (Var "D2")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "a1")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "D1"))  (Bool  "for" (Set (Var "a2")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "D2"))  (Bool  "for" (Set (Var "f1")) "being"   ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "D1"))  (Bool  "for" (Set (Var "f2")) "being"   ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "D2")) "holds"   (Bool  "("  (Bool  "("  (Bool (Set (Var "a1"))  ($#r3_binop_1 :::"is_a_unity_wrt"::: )  (Set (Var "f1"))) & (Bool (Set (Var "a2"))  ($#r3_binop_1 :::"is_a_unity_wrt"::: )  (Set (Var "f2")))  ")" ) "iff" (Bool (Set  ($#k1_domain_1 :::"["::: ) (Set (Var "a1")) "," (Set (Var "a2")) ($#k1_domain_1 :::"]"::: ) )  ($#r3_binop_1 :::"is_a_unity_wrt"::: )  (Set  ($#k6_filter_1 :::"|:"::: ) (Set (Var "f1")) "," (Set (Var "f2")) ($#k6_filter_1 :::":|"::: ) ))  ")" )))))) ; 
 
theorem :: FILTER_1:27 (Bool  "for" (Set (Var "D1")) "," (Set (Var "D2")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "f1")) "," (Set (Var "g1")) "being"   ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "D1"))  (Bool  "for" (Set (Var "f2")) "," (Set (Var "g2")) "being"   ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "D2")) "holds"   (Bool  "("  (Bool  "("  (Bool (Set (Var "f1"))  ($#r4_binop_1 :::"is_left_distributive_wrt"::: )  (Set (Var "g1"))) & (Bool (Set (Var "f2"))  ($#r4_binop_1 :::"is_left_distributive_wrt"::: )  (Set (Var "g2")))  ")" ) "iff" (Bool (Set  ($#k6_filter_1 :::"|:"::: ) (Set (Var "f1")) "," (Set (Var "f2")) ($#k6_filter_1 :::":|"::: ) )  ($#r4_binop_1 :::"is_left_distributive_wrt"::: )  (Set  ($#k6_filter_1 :::"|:"::: ) (Set (Var "g1")) "," (Set (Var "g2")) ($#k6_filter_1 :::":|"::: ) ))  ")" )))) ; 
 
theorem :: FILTER_1:28 (Bool  "for" (Set (Var "D1")) "," (Set (Var "D2")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "f1")) "," (Set (Var "g1")) "being"   ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "D1"))  (Bool  "for" (Set (Var "f2")) "," (Set (Var "g2")) "being"   ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "D2")) "holds"   (Bool  "("  (Bool  "("  (Bool (Set (Var "f1"))  ($#r5_binop_1 :::"is_right_distributive_wrt"::: )  (Set (Var "g1"))) & (Bool (Set (Var "f2"))  ($#r5_binop_1 :::"is_right_distributive_wrt"::: )  (Set (Var "g2")))  ")" ) "iff" (Bool (Set  ($#k6_filter_1 :::"|:"::: ) (Set (Var "f1")) "," (Set (Var "f2")) ($#k6_filter_1 :::":|"::: ) )  ($#r5_binop_1 :::"is_right_distributive_wrt"::: )  (Set  ($#k6_filter_1 :::"|:"::: ) (Set (Var "g1")) "," (Set (Var "g2")) ($#k6_filter_1 :::":|"::: ) ))  ")" )))) ; 
 
theorem :: FILTER_1:29 (Bool  "for" (Set (Var "D1")) "," (Set (Var "D2")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "f1")) "," (Set (Var "g1")) "being"   ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "D1"))  (Bool  "for" (Set (Var "f2")) "," (Set (Var "g2")) "being"   ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "D2")) "holds"   (Bool  "("  (Bool  "("  (Bool (Set (Var "f1"))  ($#r6_binop_1 :::"is_distributive_wrt"::: )  (Set (Var "g1"))) & (Bool (Set (Var "f2"))  ($#r6_binop_1 :::"is_distributive_wrt"::: )  (Set (Var "g2")))  ")" ) "iff" (Bool (Set  ($#k6_filter_1 :::"|:"::: ) (Set (Var "f1")) "," (Set (Var "f2")) ($#k6_filter_1 :::":|"::: ) )  ($#r6_binop_1 :::"is_distributive_wrt"::: )  (Set  ($#k6_filter_1 :::"|:"::: ) (Set (Var "g1")) "," (Set (Var "g2")) ($#k6_filter_1 :::":|"::: ) ))  ")" )))) ; 
 
theorem :: FILTER_1:30 (Bool  "for" (Set (Var "D1")) "," (Set (Var "D2")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "f1")) "," (Set (Var "g1")) "being"   ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "D1"))  (Bool  "for" (Set (Var "f2")) "," (Set (Var "g2")) "being"   ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "D2")) "holds"   (Bool  "("  (Bool  "("  (Bool (Set (Var "f1"))  ($#r1_lattice2 :::"absorbs"::: )  (Set (Var "g1"))) & (Bool (Set (Var "f2"))  ($#r1_lattice2 :::"absorbs"::: )  (Set (Var "g2")))  ")" ) "iff" (Bool (Set  ($#k6_filter_1 :::"|:"::: ) (Set (Var "f1")) "," (Set (Var "f2")) ($#k6_filter_1 :::":|"::: ) )  ($#r1_lattice2 :::"absorbs"::: )  (Set  ($#k6_filter_1 :::"|:"::: ) (Set (Var "g1")) "," (Set (Var "g2")) ($#k6_filter_1 :::":|"::: ) ))  ")" )))) ; 
 definitionlet "L1", "L2" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l3_lattices :::"LattStr"::: )  ; func :::"[:":::"L1" "," "L2":::":]"::: ->   ($#v3_lattices :::"strict"::: )     ($#l3_lattices :::"LattStr"::: )   equals :: FILTER_1:def 7 (Set   ($#g3_lattices :::"LattStr"::: )  "(#"  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "L1") "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "L2") ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set  ($#k6_filter_1 :::"|:"::: ) (Set  "the"  ($#u2_lattices :::"L_join"::: )  "of" "L1") "," (Set  "the"  ($#u2_lattices :::"L_join"::: )  "of" "L2") ($#k6_filter_1 :::":|"::: ) ) "," (Set  ($#k6_filter_1 :::"|:"::: ) (Set  "the"  ($#u1_lattices :::"L_meet"::: )  "of" "L1") "," (Set  "the"  ($#u1_lattices :::"L_meet"::: )  "of" "L2") ($#k6_filter_1 :::":|"::: ) ) "#)" ); end; 






:: deftheorem    defines :::"[:"::: FILTER_1:def 7 :  (Bool  "for" (Set (Var "L1")) "," (Set (Var "L2")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l3_lattices :::"LattStr"::: )   "holds"  (Bool (Set  ($#k7_filter_1 :::"[:"::: ) (Set (Var "L1")) "," (Set (Var "L2")) ($#k7_filter_1 :::":]"::: ) )  ($#r1_hidden :::"="::: )  (Set   ($#g3_lattices :::"LattStr"::: )  "(#"  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "L1"))) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "L2"))) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set  ($#k6_filter_1 :::"|:"::: ) (Set  "the"  ($#u2_lattices :::"L_join"::: )  "of" (Set (Var "L1"))) "," (Set  "the"  ($#u2_lattices :::"L_join"::: )  "of" (Set (Var "L2"))) ($#k6_filter_1 :::":|"::: ) ) "," (Set  ($#k6_filter_1 :::"|:"::: ) (Set  "the"  ($#u1_lattices :::"L_meet"::: )  "of" (Set (Var "L1"))) "," (Set  "the"  ($#u1_lattices :::"L_meet"::: )  "of" (Set (Var "L2"))) ($#k6_filter_1 :::":|"::: ) ) "#)" ))); 
 registrationlet "L1", "L2" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l3_lattices :::"LattStr"::: )  ; 
cluster (Set  ($#k7_filter_1 :::"[:"::: ) "L1" "," "L2" ($#k7_filter_1 :::":]"::: ) ) ->  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v3_lattices :::"strict"::: )   ; 
end; definitionlet "L" be   ($#l3_lattices :::"Lattice":::); func  :::"LattRel"::: "L" ->   ($#m1_hidden :::"Relation":::) equals :: FILTER_1:def 8  "{"  (Set  ($#k1_domain_1 :::"["::: ) (Set (Var "p")) "," (Set (Var "q")) ($#k1_domain_1 :::"]"::: ) ) where p, q "is"   ($#m1_subset_1 :::"Element":::) "of" "L" : (Bool (Set (Var "p"))  ($#r3_lattices :::"[="::: )  (Set (Var "q")))  "}"  ; end; 





:: deftheorem    defines :::"LattRel"::: FILTER_1:def 8 :  (Bool  "for" (Set (Var "L")) "being"   ($#l3_lattices :::"Lattice":::) "holds"  (Bool (Set   ($#k8_filter_1 :::"LattRel"::: )  (Set (Var "L")))  ($#r1_hidden :::"="::: )   "{"  (Set  ($#k1_domain_1 :::"["::: ) (Set (Var "p")) "," (Set (Var "q")) ($#k1_domain_1 :::"]"::: ) ) where p, q "is"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) : (Bool (Set (Var "p"))  ($#r3_lattices :::"[="::: )  (Set (Var "q")))  "}"  )); 
 
theorem :: FILTER_1:31 (Bool  "for" (Set (Var "L")) "being"   ($#l3_lattices :::"Lattice":::)  (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"   (Bool  "("  (Bool (Set  ($#k1_domain_1 :::"["::: ) (Set (Var "p")) "," (Set (Var "q")) ($#k1_domain_1 :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set   ($#k8_filter_1 :::"LattRel"::: )  (Set (Var "L")))) "iff" (Bool (Set (Var "p"))  ($#r3_lattices :::"[="::: )  (Set (Var "q")))  ")" ))) ; 
 
theorem :: FILTER_1:32 (Bool  "for" (Set (Var "L")) "being"   ($#l3_lattices :::"Lattice":::) "holds"   (Bool  "("  (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set  "("  ($#k8_filter_1 :::"LattRel"::: )  (Set (Var "L")) ")" ))  ($#r1_hidden :::"="::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "L")))) & (Bool (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set  "("  ($#k8_filter_1 :::"LattRel"::: )  (Set (Var "L")) ")" ))  ($#r1_hidden :::"="::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "L")))) & (Bool (Set   ($#k1_relat_1 :::"field"::: )  (Set  "("  ($#k8_filter_1 :::"LattRel"::: )  (Set (Var "L")) ")" ))  ($#r1_hidden :::"="::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "L"))))  ")" )) ; 
 definitionlet "L1", "L2" be   ($#l3_lattices :::"Lattice":::); pred "L1" "," "L2" :::"are_isomorphic":::  means :: FILTER_1:def 9 (Bool (Set   ($#k8_filter_1 :::"LattRel"::: )  "L1") "," (Set   ($#k8_filter_1 :::"LattRel"::: )  "L2")  ($#r4_wellord1 :::"are_isomorphic"::: )  ); reflexivity  
(Bool  "for" (Set (Var "L1")) "being"   ($#l3_lattices :::"Lattice":::) "holds"  (Bool (Set   ($#k8_filter_1 :::"LattRel"::: )  (Set (Var "L1"))) "," (Set   ($#k8_filter_1 :::"LattRel"::: )  (Set (Var "L1")))  ($#r4_wellord1 :::"are_isomorphic"::: )  ))
 ; symmetry  
(Bool  "for" (Set (Var "L1")) "," (Set (Var "L2")) "being"   ($#l3_lattices :::"Lattice":::)  "st" (Bool (Bool (Set   ($#k8_filter_1 :::"LattRel"::: )  (Set (Var "L1"))) "," (Set   ($#k8_filter_1 :::"LattRel"::: )  (Set (Var "L2")))  ($#r4_wellord1 :::"are_isomorphic"::: )  )) "holds"  (Bool (Set   ($#k8_filter_1 :::"LattRel"::: )  (Set (Var "L2"))) "," (Set   ($#k8_filter_1 :::"LattRel"::: )  (Set (Var "L1")))  ($#r4_wellord1 :::"are_isomorphic"::: )  ))
 ; end; 





:: deftheorem    defines :::"are_isomorphic"::: FILTER_1:def 9 :  (Bool  "for" (Set (Var "L1")) "," (Set (Var "L2")) "being"   ($#l3_lattices :::"Lattice":::) "holds"   (Bool  "("  (Bool (Set (Var "L1")) "," (Set (Var "L2"))  ($#r1_filter_1 :::"are_isomorphic"::: )  ) "iff" (Bool (Set   ($#k8_filter_1 :::"LattRel"::: )  (Set (Var "L1"))) "," (Set   ($#k8_filter_1 :::"LattRel"::: )  (Set (Var "L2")))  ($#r4_wellord1 :::"are_isomorphic"::: )  )  ")" )); 
 registrationlet "L1", "L2" be   ($#l3_lattices :::"Lattice":::); 
cluster (Set  ($#k7_filter_1 :::"[:"::: ) "L1" "," "L2" ($#k7_filter_1 :::":]"::: ) ) ->   ($#v3_lattices :::"strict"::: )     ($#v10_lattices :::"Lattice-like"::: )   ; 
end; 
theorem :: FILTER_1:33 (Bool  "for" (Set (Var "L1")) "," (Set (Var "L2")) "," (Set (Var "L3")) "being"   ($#l3_lattices :::"Lattice":::)  "st" (Bool (Bool (Set (Var "L1")) "," (Set (Var "L2"))  ($#r1_filter_1 :::"are_isomorphic"::: )  ) & (Bool (Set (Var "L2")) "," (Set (Var "L3"))  ($#r1_filter_1 :::"are_isomorphic"::: )  )) "holds"  (Bool (Set (Var "L1")) "," (Set (Var "L3"))  ($#r1_filter_1 :::"are_isomorphic"::: )  )) ; 
 
theorem :: FILTER_1:34 (Bool  "for" (Set (Var "L1")) "," (Set (Var "L2")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l3_lattices :::"LattStr"::: )    "st" (Bool (Bool (Set  ($#k7_filter_1 :::"[:"::: ) (Set (Var "L1")) "," (Set (Var "L2")) ($#k7_filter_1 :::":]"::: ) ) "is"   ($#l3_lattices :::"Lattice":::))) "holds"  (Bool  "("  (Bool (Set (Var "L1")) "is"   ($#l3_lattices :::"Lattice":::)) & (Bool (Set (Var "L2")) "is"   ($#l3_lattices :::"Lattice":::))  ")" )) ; 
 definitionlet "L1", "L2" be   ($#l3_lattices :::"Lattice":::); let "a" be   ($#m1_subset_1 :::"Element":::) "of" (Set (Const "L1")); let "b" be   ($#m1_subset_1 :::"Element":::) "of" (Set (Const "L2")); :: original: :::"["::: redefine func :::"[":::"a" "," "b":::"]"::: ->   ($#m1_subset_1 :::"Element":::) "of" (Set  ($#k7_filter_1 :::"[:"::: ) "L1" "," "L2" ($#k7_filter_1 :::":]"::: ) ); end; 
theorem :: FILTER_1:35 (Bool  "for" (Set (Var "L1")) "," (Set (Var "L2")) "being"   ($#l3_lattices :::"Lattice":::)  (Bool  "for" (Set (Var "p1")) "," (Set (Var "q1")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L1"))  (Bool  "for" (Set (Var "p2")) "," (Set (Var "q2")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L2")) "holds"   (Bool  "("  (Bool (Set (Set  ($#k9_filter_1 :::"["::: ) (Set (Var "p1")) "," (Set (Var "p2")) ($#k9_filter_1 :::"]"::: ) )  ($#k3_lattices :::""\/""::: )  (Set  ($#k9_filter_1 :::"["::: ) (Set (Var "q1")) "," (Set (Var "q2")) ($#k9_filter_1 :::"]"::: ) ))  ($#r1_hidden :::"="::: )  (Set  ($#k9_filter_1 :::"["::: ) (Set  "(" (Set (Var "p1"))  ($#k3_lattices :::""\/""::: )  (Set (Var "q1")) ")" ) "," (Set  "(" (Set (Var "p2"))  ($#k3_lattices :::""\/""::: )  (Set (Var "q2")) ")" ) ($#k9_filter_1 :::"]"::: ) )) & (Bool (Set (Set  ($#k9_filter_1 :::"["::: ) (Set (Var "p1")) "," (Set (Var "p2")) ($#k9_filter_1 :::"]"::: ) )  ($#k4_lattices :::""/\""::: )  (Set  ($#k9_filter_1 :::"["::: ) (Set (Var "q1")) "," (Set (Var "q2")) ($#k9_filter_1 :::"]"::: ) ))  ($#r1_hidden :::"="::: )  (Set  ($#k9_filter_1 :::"["::: ) (Set  "(" (Set (Var "p1"))  ($#k4_lattices :::""/\""::: )  (Set (Var "q1")) ")" ) "," (Set  "(" (Set (Var "p2"))  ($#k4_lattices :::""/\""::: )  (Set (Var "q2")) ")" ) ($#k9_filter_1 :::"]"::: ) ))  ")" )))) ; 
 
theorem :: FILTER_1:36 (Bool  "for" (Set (Var "L1")) "," (Set (Var "L2")) "being"   ($#l3_lattices :::"Lattice":::)  (Bool  "for" (Set (Var "p1")) "," (Set (Var "q1")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L1"))  (Bool  "for" (Set (Var "p2")) "," (Set (Var "q2")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L2")) "holds"   (Bool  "("  (Bool (Set  ($#k9_filter_1 :::"["::: ) (Set (Var "p1")) "," (Set (Var "p2")) ($#k9_filter_1 :::"]"::: ) )  ($#r3_lattices :::"[="::: )  (Set  ($#k9_filter_1 :::"["::: ) (Set (Var "q1")) "," (Set (Var "q2")) ($#k9_filter_1 :::"]"::: ) )) "iff" (Bool  "("  (Bool (Set (Var "p1"))  ($#r3_lattices :::"[="::: )  (Set (Var "q1"))) & (Bool (Set (Var "p2"))  ($#r3_lattices :::"[="::: )  (Set (Var "q2")))  ")" )  ")" )))) ; 
 
theorem :: FILTER_1:37 (Bool  "for" (Set (Var "L1")) "," (Set (Var "L2")) "being"   ($#l3_lattices :::"Lattice":::) "holds"   (Bool  "("  (Bool  "("  (Bool (Set (Var "L1")) "is"   ($#v12_lattices :::"modular"::: )  ) & (Bool (Set (Var "L2")) "is"   ($#v12_lattices :::"modular"::: )  )  ")" ) "iff" (Bool (Set  ($#k7_filter_1 :::"[:"::: ) (Set (Var "L1")) "," (Set (Var "L2")) ($#k7_filter_1 :::":]"::: ) ) "is"   ($#v12_lattices :::"modular"::: )  )  ")" )) ; 
 
theorem :: FILTER_1:38 (Bool  "for" (Set (Var "L1")) "," (Set (Var "L2")) "being"   ($#l3_lattices :::"Lattice":::) "holds"   (Bool  "("  (Bool  "("  (Bool (Set (Var "L1")) "is"   ($#l3_lattices :::"D_Lattice":::)) & (Bool (Set (Var "L2")) "is"   ($#l3_lattices :::"D_Lattice":::))  ")" ) "iff" (Bool (Set  ($#k7_filter_1 :::"[:"::: ) (Set (Var "L1")) "," (Set (Var "L2")) ($#k7_filter_1 :::":]"::: ) ) "is"   ($#l3_lattices :::"D_Lattice":::))  ")" )) ; 
 
theorem :: FILTER_1:39 (Bool  "for" (Set (Var "L1")) "," (Set (Var "L2")) "being"   ($#l3_lattices :::"Lattice":::) "holds"   (Bool  "("  (Bool  "("  (Bool (Set (Var "L1")) "is"   ($#v13_lattices :::"lower-bounded"::: )  ) & (Bool (Set (Var "L2")) "is"   ($#v13_lattices :::"lower-bounded"::: )  )  ")" ) "iff" (Bool (Set  ($#k7_filter_1 :::"[:"::: ) (Set (Var "L1")) "," (Set (Var "L2")) ($#k7_filter_1 :::":]"::: ) ) "is"   ($#v13_lattices :::"lower-bounded"::: )  )  ")" )) ; 
 
theorem :: FILTER_1:40 (Bool  "for" (Set (Var "L1")) "," (Set (Var "L2")) "being"   ($#l3_lattices :::"Lattice":::) "holds"   (Bool  "("  (Bool  "("  (Bool (Set (Var "L1")) "is"   ($#v14_lattices :::"upper-bounded"::: )  ) & (Bool (Set (Var "L2")) "is"   ($#v14_lattices :::"upper-bounded"::: )  )  ")" ) "iff" (Bool (Set  ($#k7_filter_1 :::"[:"::: ) (Set (Var "L1")) "," (Set (Var "L2")) ($#k7_filter_1 :::":]"::: ) ) "is"   ($#v14_lattices :::"upper-bounded"::: )  )  ")" )) ; 
 
theorem :: FILTER_1:41 (Bool  "for" (Set (Var "L1")) "," (Set (Var "L2")) "being"   ($#l3_lattices :::"Lattice":::) "holds"   (Bool  "("  (Bool  "("  (Bool (Set (Var "L1")) "is"   ($#v15_lattices :::"bounded"::: )  ) & (Bool (Set (Var "L2")) "is"   ($#v15_lattices :::"bounded"::: )  )  ")" ) "iff" (Bool (Set  ($#k7_filter_1 :::"[:"::: ) (Set (Var "L1")) "," (Set (Var "L2")) ($#k7_filter_1 :::":]"::: ) ) "is"   ($#v15_lattices :::"bounded"::: )  )  ")" )) ; 
 
theorem :: FILTER_1:42 (Bool  "for" (Set (Var "L1")) "," (Set (Var "L2")) "being"   ($#l3_lattices :::"Lattice":::)  "st" (Bool (Bool (Set (Var "L1")) "is"   ($#l3_lattices :::"0_Lattice":::)) & (Bool (Set (Var "L2")) "is"   ($#l3_lattices :::"0_Lattice":::))) "holds"  (Bool (Set   ($#k5_lattices :::"Bottom"::: )  (Set  ($#k7_filter_1 :::"[:"::: ) (Set (Var "L1")) "," (Set (Var "L2")) ($#k7_filter_1 :::":]"::: ) ))  ($#r1_hidden :::"="::: )  (Set  ($#k9_filter_1 :::"["::: ) (Set  "("  ($#k5_lattices :::"Bottom"::: )  (Set (Var "L1")) ")" ) "," (Set  "("  ($#k5_lattices :::"Bottom"::: )  (Set (Var "L2")) ")" ) ($#k9_filter_1 :::"]"::: ) ))) ; 
 
theorem :: FILTER_1:43 (Bool  "for" (Set (Var "L1")) "," (Set (Var "L2")) "being"   ($#l3_lattices :::"Lattice":::)  "st" (Bool (Bool (Set (Var "L1")) "is"   ($#l3_lattices :::"1_Lattice":::)) & (Bool (Set (Var "L2")) "is"   ($#l3_lattices :::"1_Lattice":::))) "holds"  (Bool (Set   ($#k6_lattices :::"Top"::: )  (Set  ($#k7_filter_1 :::"[:"::: ) (Set (Var "L1")) "," (Set (Var "L2")) ($#k7_filter_1 :::":]"::: ) ))  ($#r1_hidden :::"="::: )  (Set  ($#k9_filter_1 :::"["::: ) (Set  "("  ($#k6_lattices :::"Top"::: )  (Set (Var "L1")) ")" ) "," (Set  "("  ($#k6_lattices :::"Top"::: )  (Set (Var "L2")) ")" ) ($#k9_filter_1 :::"]"::: ) ))) ; 
 
theorem :: FILTER_1:44 (Bool  "for" (Set (Var "L1")) "," (Set (Var "L2")) "being"   ($#l3_lattices :::"Lattice":::)  (Bool  "for" (Set (Var "p1")) "," (Set (Var "q1")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L1"))  (Bool  "for" (Set (Var "p2")) "," (Set (Var "q2")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L2"))  "st" (Bool (Bool (Set (Var "L1")) "is"   ($#l3_lattices :::"01_Lattice":::)) & (Bool (Set (Var "L2")) "is"   ($#l3_lattices :::"01_Lattice":::))) "holds"  (Bool  "("  (Bool  "("  (Bool (Set (Var "p1"))  ($#r2_lattices :::"is_a_complement_of"::: )  (Set (Var "q1"))) & (Bool (Set (Var "p2"))  ($#r2_lattices :::"is_a_complement_of"::: )  (Set (Var "q2")))  ")" ) "iff" (Bool (Set  ($#k9_filter_1 :::"["::: ) (Set (Var "p1")) "," (Set (Var "p2")) ($#k9_filter_1 :::"]"::: ) )  ($#r2_lattices :::"is_a_complement_of"::: )  (Set  ($#k9_filter_1 :::"["::: ) (Set (Var "q1")) "," (Set (Var "q2")) ($#k9_filter_1 :::"]"::: ) ))  ")" )))) ; 
 
theorem :: FILTER_1:45 (Bool  "for" (Set (Var "L1")) "," (Set (Var "L2")) "being"   ($#l3_lattices :::"Lattice":::) "holds"   (Bool  "("  (Bool  "("  (Bool (Set (Var "L1")) "is"   ($#l3_lattices :::"C_Lattice":::)) & (Bool (Set (Var "L2")) "is"   ($#l3_lattices :::"C_Lattice":::))  ")" ) "iff" (Bool (Set  ($#k7_filter_1 :::"[:"::: ) (Set (Var "L1")) "," (Set (Var "L2")) ($#k7_filter_1 :::":]"::: ) ) "is"   ($#l3_lattices :::"C_Lattice":::))  ")" )) ; 
 
theorem :: FILTER_1:46 (Bool  "for" (Set (Var "L1")) "," (Set (Var "L2")) "being"   ($#l3_lattices :::"Lattice":::) "holds"   (Bool  "("  (Bool  "("  (Bool (Set (Var "L1")) "is"   ($#l3_lattices :::"B_Lattice":::)) & (Bool (Set (Var "L2")) "is"   ($#l3_lattices :::"B_Lattice":::))  ")" ) "iff" (Bool (Set  ($#k7_filter_1 :::"[:"::: ) (Set (Var "L1")) "," (Set (Var "L2")) ($#k7_filter_1 :::":]"::: ) ) "is"   ($#l3_lattices :::"B_Lattice":::))  ")" )) ; 
 
theorem :: FILTER_1:47 (Bool  "for" (Set (Var "L1")) "," (Set (Var "L2")) "being"   ($#l3_lattices :::"Lattice":::) "holds"   (Bool  "("  (Bool  "("  (Bool (Set (Var "L1")) "is"   ($#v3_filter_0 :::"implicative"::: )  ) & (Bool (Set (Var "L2")) "is"   ($#v3_filter_0 :::"implicative"::: )  )  ")" ) "iff" (Bool (Set  ($#k7_filter_1 :::"[:"::: ) (Set (Var "L1")) "," (Set (Var "L2")) ($#k7_filter_1 :::":]"::: ) ) "is"   ($#v3_filter_0 :::"implicative"::: )  )  ")" )) ; 
 
theorem :: FILTER_1:48 (Bool  "for" (Set (Var "L1")) "," (Set (Var "L2")) "being"   ($#l3_lattices :::"Lattice":::) "holds"  (Bool (Set (Set  ($#k7_filter_1 :::"[:"::: ) (Set (Var "L1")) "," (Set (Var "L2")) ($#k7_filter_1 :::":]"::: ) )  ($#k1_lattice2 :::".:"::: )  )  ($#r1_hidden :::"="::: )  (Set  ($#k7_filter_1 :::"[:"::: ) (Set  "(" (Set (Var "L1"))  ($#k1_lattice2 :::".:"::: )  ")" ) "," (Set  "(" (Set (Var "L2"))  ($#k1_lattice2 :::".:"::: )  ")" ) ($#k7_filter_1 :::":]"::: ) ))) ; 
 
theorem :: FILTER_1:49 (Bool  "for" (Set (Var "L1")) "," (Set (Var "L2")) "being"   ($#l3_lattices :::"Lattice":::) "holds"  (Bool (Set  ($#k7_filter_1 :::"[:"::: ) (Set (Var "L1")) "," (Set (Var "L2")) ($#k7_filter_1 :::":]"::: ) ) "," (Set  ($#k7_filter_1 :::"[:"::: ) (Set (Var "L2")) "," (Set (Var "L1")) ($#k7_filter_1 :::":]"::: ) )  ($#r1_filter_1 :::"are_isomorphic"::: )  )) ; 
 









theorem :: FILTER_1:50 (Bool  "for" (Set (Var "B")) "being"   ($#l3_lattices :::"B_Lattice":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "B")) "holds"  (Bool (Set (Set (Var "a"))  ($#k7_filter_0 :::"<=>"::: )  (Set (Var "b")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "a"))  ($#k4_lattices :::""/\""::: )  (Set (Var "b")) ")" )  ($#k3_lattices :::""\/""::: )  (Set  "(" (Set  "(" (Set (Var "a"))  ($#k7_lattices :::"`"::: )  ")" )  ($#k4_lattices :::""/\""::: )  (Set  "(" (Set (Var "b"))  ($#k7_lattices :::"`"::: )  ")" ) ")" ))))) ; 
 
theorem :: FILTER_1:51 (Bool  "for" (Set (Var "B")) "being"   ($#l3_lattices :::"B_Lattice":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "B")) "holds"   (Bool  "("  (Bool (Set (Set  "(" (Set (Var "a"))  ($#k4_filter_0 :::"=>"::: )  (Set (Var "b")) ")" )  ($#k7_lattices :::"`"::: )  )  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k4_lattices :::""/\""::: )  (Set  "(" (Set (Var "b"))  ($#k7_lattices :::"`"::: )  ")" ))) & (Bool (Set (Set  "(" (Set (Var "a"))  ($#k7_filter_0 :::"<=>"::: )  (Set (Var "b")) ")" )  ($#k7_lattices :::"`"::: )  )  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "a"))  ($#k4_lattices :::""/\""::: )  (Set  "(" (Set (Var "b"))  ($#k7_lattices :::"`"::: )  ")" ) ")" )  ($#k3_lattices :::""\/""::: )  (Set  "(" (Set  "(" (Set (Var "a"))  ($#k7_lattices :::"`"::: )  ")" )  ($#k4_lattices :::""/\""::: )  (Set (Var "b")) ")" ))) & (Bool (Set (Set  "(" (Set (Var "a"))  ($#k7_filter_0 :::"<=>"::: )  (Set (Var "b")) ")" )  ($#k7_lattices :::"`"::: )  )  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k7_filter_0 :::"<=>"::: )  (Set  "(" (Set (Var "b"))  ($#k7_lattices :::"`"::: )  ")" ))) & (Bool (Set (Set  "(" (Set (Var "a"))  ($#k7_filter_0 :::"<=>"::: )  (Set (Var "b")) ")" )  ($#k7_lattices :::"`"::: )  )  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "a"))  ($#k7_lattices :::"`"::: )  ")" )  ($#k7_filter_0 :::"<=>"::: )  (Set (Var "b"))))  ")" ))) ; 
 
theorem :: FILTER_1:52 (Bool  "for" (Set (Var "B")) "being"   ($#l3_lattices :::"B_Lattice":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "B"))  "st" (Bool (Bool (Set (Set (Var "a"))  ($#k7_filter_0 :::"<=>"::: )  (Set (Var "b")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k7_filter_0 :::"<=>"::: )  (Set (Var "c"))))) "holds"  (Bool (Set (Var "b"))  ($#r1_hidden :::"="::: )  (Set (Var "c"))))) ; 
 
theorem :: FILTER_1:53 (Bool  "for" (Set (Var "B")) "being"   ($#l3_lattices :::"B_Lattice":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "B")) "holds"  (Bool (Set (Set (Var "a"))  ($#k7_filter_0 :::"<=>"::: )  (Set  "(" (Set (Var "a"))  ($#k7_filter_0 :::"<=>"::: )  (Set (Var "b")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "b"))))) ; 
 
theorem :: FILTER_1:54 (Bool  "for" (Set (Var "I")) "being"   ($#l3_lattices :::"I_Lattice":::)  (Bool  "for" (Set (Var "i")) "," (Set (Var "j")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "I")) "holds"   (Bool  "("  (Bool (Set (Set  "(" (Set (Var "i"))  ($#k3_lattices :::""\/""::: )  (Set (Var "j")) ")" )  ($#k4_filter_0 :::"=>"::: )  (Set (Var "i")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "j"))  ($#k4_filter_0 :::"=>"::: )  (Set (Var "i")))) & (Bool (Set (Set (Var "i"))  ($#k4_filter_0 :::"=>"::: )  (Set  "(" (Set (Var "i"))  ($#k4_lattices :::""/\""::: )  (Set (Var "j")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "i"))  ($#k4_filter_0 :::"=>"::: )  (Set (Var "j"))))  ")" ))) ; 
 
theorem :: FILTER_1:55 (Bool  "for" (Set (Var "I")) "being"   ($#l3_lattices :::"I_Lattice":::)  (Bool  "for" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "k")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "I")) "holds"   (Bool  "("  (Bool (Set (Set (Var "i"))  ($#k4_filter_0 :::"=>"::: )  (Set (Var "j")))  ($#r3_lattices :::"[="::: )  (Set (Set (Var "i"))  ($#k4_filter_0 :::"=>"::: )  (Set  "(" (Set (Var "j"))  ($#k3_lattices :::""\/""::: )  (Set (Var "k")) ")" ))) & (Bool (Set (Set (Var "i"))  ($#k4_filter_0 :::"=>"::: )  (Set (Var "j")))  ($#r3_lattices :::"[="::: )  (Set (Set  "(" (Set (Var "i"))  ($#k4_lattices :::""/\""::: )  (Set (Var "k")) ")" )  ($#k4_filter_0 :::"=>"::: )  (Set (Var "j")))) & (Bool (Set (Set (Var "i"))  ($#k4_filter_0 :::"=>"::: )  (Set (Var "j")))  ($#r3_lattices :::"[="::: )  (Set (Set (Var "i"))  ($#k4_filter_0 :::"=>"::: )  (Set  "(" (Set (Var "k"))  ($#k3_lattices :::""\/""::: )  (Set (Var "j")) ")" ))) & (Bool (Set (Set (Var "i"))  ($#k4_filter_0 :::"=>"::: )  (Set (Var "j")))  ($#r3_lattices :::"[="::: )  (Set (Set  "(" (Set (Var "k"))  ($#k4_lattices :::""/\""::: )  (Set (Var "i")) ")" )  ($#k4_filter_0 :::"=>"::: )  (Set (Var "j"))))  ")" ))) ; 
 
theorem :: FILTER_1:56 (Bool  "for" (Set (Var "I")) "being"   ($#l3_lattices :::"I_Lattice":::)  (Bool  "for" (Set (Var "i")) "," (Set (Var "k")) "," (Set (Var "j")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "I")) "holds"  (Bool (Set (Set  "(" (Set (Var "i"))  ($#k4_filter_0 :::"=>"::: )  (Set (Var "k")) ")" )  ($#k4_lattices :::""/\""::: )  (Set  "(" (Set (Var "j"))  ($#k4_filter_0 :::"=>"::: )  (Set (Var "k")) ")" ))  ($#r3_lattices :::"[="::: )  (Set (Set  "(" (Set (Var "i"))  ($#k3_lattices :::""\/""::: )  (Set (Var "j")) ")" )  ($#k4_filter_0 :::"=>"::: )  (Set (Var "k")))))) ; 
 
theorem :: FILTER_1:57 (Bool  "for" (Set (Var "I")) "being"   ($#l3_lattices :::"I_Lattice":::)  (Bool  "for" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "k")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "I")) "holds"  (Bool (Set (Set  "(" (Set (Var "i"))  ($#k4_filter_0 :::"=>"::: )  (Set (Var "j")) ")" )  ($#k4_lattices :::""/\""::: )  (Set  "(" (Set (Var "i"))  ($#k4_filter_0 :::"=>"::: )  (Set (Var "k")) ")" ))  ($#r3_lattices :::"[="::: )  (Set (Set (Var "i"))  ($#k4_filter_0 :::"=>"::: )  (Set  "(" (Set (Var "j"))  ($#k4_lattices :::""/\""::: )  (Set (Var "k")) ")" ))))) ; 
 
theorem :: FILTER_1:58 (Bool  "for" (Set (Var "I")) "being"   ($#l3_lattices :::"I_Lattice":::)  (Bool  "for" (Set (Var "FI")) "being"   ($#m1_subset_1 :::"Filter":::) "of" (Set (Var "I"))  (Bool  "for" (Set (Var "i1")) "," (Set (Var "i2")) "," (Set (Var "j1")) "," (Set (Var "j2")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "I"))  "st" (Bool (Bool (Set (Set (Var "i1"))  ($#k7_filter_0 :::"<=>"::: )  (Set (Var "i2")))  ($#r2_hidden :::"in"::: )  (Set (Var "FI"))) & (Bool (Set (Set (Var "j1"))  ($#k7_filter_0 :::"<=>"::: )  (Set (Var "j2")))  ($#r2_hidden :::"in"::: )  (Set (Var "FI")))) "holds"  (Bool  "("  (Bool (Set (Set  "(" (Set (Var "i1"))  ($#k3_lattices :::""\/""::: )  (Set (Var "j1")) ")" )  ($#k7_filter_0 :::"<=>"::: )  (Set  "(" (Set (Var "i2"))  ($#k3_lattices :::""\/""::: )  (Set (Var "j2")) ")" ))  ($#r2_hidden :::"in"::: )  (Set (Var "FI"))) & (Bool (Set (Set  "(" (Set (Var "i1"))  ($#k4_lattices :::""/\""::: )  (Set (Var "j1")) ")" )  ($#k7_filter_0 :::"<=>"::: )  (Set  "(" (Set (Var "i2"))  ($#k4_lattices :::""/\""::: )  (Set (Var "j2")) ")" ))  ($#r2_hidden :::"in"::: )  (Set (Var "FI")))  ")" )))) ; 
 
theorem :: FILTER_1:59 (Bool  "for" (Set (Var "I")) "being"   ($#l3_lattices :::"I_Lattice":::)  (Bool  "for" (Set (Var "FI")) "being"   ($#m1_subset_1 :::"Filter":::) "of" (Set (Var "I"))  (Bool  "for" (Set (Var "i")) "," (Set (Var "k")) "," (Set (Var "j")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "I"))  "st" (Bool (Bool (Set (Var "i"))  ($#r2_hidden :::"in"::: )  (Set   ($#k6_eqrel_1 :::"Class"::: )   "(" (Set  "("  ($#k9_filter_0 :::"equivalence_wrt"::: )  (Set (Var "FI")) ")" ) "," (Set (Var "k")) ")" )) & (Bool (Set (Var "j"))  ($#r2_hidden :::"in"::: )  (Set   ($#k6_eqrel_1 :::"Class"::: )   "(" (Set  "("  ($#k9_filter_0 :::"equivalence_wrt"::: )  (Set (Var "FI")) ")" ) "," (Set (Var "k")) ")" ))) "holds"  (Bool  "("  (Bool (Set (Set (Var "i"))  ($#k3_lattices :::""\/""::: )  (Set (Var "j")))  ($#r2_hidden :::"in"::: )  (Set   ($#k6_eqrel_1 :::"Class"::: )   "(" (Set  "("  ($#k9_filter_0 :::"equivalence_wrt"::: )  (Set (Var "FI")) ")" ) "," (Set (Var "k")) ")" )) & (Bool (Set (Set (Var "i"))  ($#k4_lattices :::""/\""::: )  (Set (Var "j")))  ($#r2_hidden :::"in"::: )  (Set   ($#k6_eqrel_1 :::"Class"::: )   "(" (Set  "("  ($#k9_filter_0 :::"equivalence_wrt"::: )  (Set (Var "FI")) ")" ) "," (Set (Var "k")) ")" ))  ")" )))) ; 
 
theorem :: FILTER_1:60 (Bool  "for" (Set (Var "B")) "being"   ($#l3_lattices :::"B_Lattice":::)  (Bool  "for" (Set (Var "c")) "," (Set (Var "d")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "B")) "holds"   (Bool  "("  (Bool (Set (Set (Var "c"))  ($#k3_lattices :::""\/""::: )  (Set  "(" (Set (Var "c"))  ($#k7_filter_0 :::"<=>"::: )  (Set (Var "d")) ")" ))  ($#r2_hidden :::"in"::: )  (Set   ($#k6_eqrel_1 :::"Class"::: )   "(" (Set  "("  ($#k10_filter_0 :::"equivalence_wrt"::: )  (Set  ($#k2_filter_0 :::"<."::: ) (Set (Var "d")) ($#k2_filter_0 :::".)"::: ) ) ")" ) "," (Set (Var "c")) ")" )) & (Bool  "("   "for" (Set (Var "b")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "B"))  "st" (Bool (Bool (Set (Var "b"))  ($#r2_hidden :::"in"::: )  (Set   ($#k6_eqrel_1 :::"Class"::: )   "(" (Set  "("  ($#k10_filter_0 :::"equivalence_wrt"::: )  (Set  ($#k2_filter_0 :::"<."::: ) (Set (Var "d")) ($#k2_filter_0 :::".)"::: ) ) ")" ) "," (Set (Var "c")) ")" ))) "holds"  (Bool (Set (Var "b"))  ($#r3_lattices :::"[="::: )  (Set (Set (Var "c"))  ($#k3_lattices :::""\/""::: )  (Set  "(" (Set (Var "c"))  ($#k7_filter_0 :::"<=>"::: )  (Set (Var "d")) ")" )))  ")" )  ")" ))) ; 
 
theorem :: FILTER_1:61 (Bool  "for" (Set (Var "B")) "being"   ($#l3_lattices :::"B_Lattice":::)  (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "B")) "holds"  (Bool (Set (Var "B")) "," (Set  ($#k7_filter_1 :::"[:"::: ) (Set  "(" (Set (Var "B"))  ($#k4_filter_1 :::"/\/"::: )  (Set  ($#k2_filter_0 :::"<."::: ) (Set (Var "a")) ($#k2_filter_0 :::".)"::: ) ) ")" ) "," (Set  "("  ($#k6_filter_0 :::"latt"::: )  (Set  ($#k2_filter_0 :::"<."::: ) (Set (Var "a")) ($#k2_filter_0 :::".)"::: ) ) ")" ) ($#k7_filter_1 :::":]"::: ) )  ($#r1_filter_1 :::"are_isomorphic"::: )  ))) ;