:: WAYBEL_1 semantic presentation begin definitionlet "L1", "L2" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_struct_0 :::"1-sorted"::: ) ; let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "L1")) "," (Set (Const "L2")); :: original: :::"one-to-one"::: redefine attr "f" is :::"one-to-one"::: means :: WAYBEL_1:def 1 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" "L1" "st" (Bool (Bool (Set "f" ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set "f" ($#k3_funct_2 :::"."::: ) (Set (Var "y"))))) "holds" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "y")))); end; :: deftheorem defines :::"one-to-one"::: WAYBEL_1:def 1 : (Bool "for" (Set (Var "L1")) "," (Set (Var "L2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_struct_0 :::"1-sorted"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "L1")) "," (Set (Var "L2")) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v2_funct_1 :::"one-to-one"::: ) ) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L1")) "st" (Bool (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "y"))))) "holds" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "y")))) ")" ))); definitionlet "L1", "L2" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) ; let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "L1")) "," (Set (Const "L2")); redefine attr "f" is :::"monotone"::: means :: WAYBEL_1:def 2 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" "L1" "st" (Bool (Bool (Set (Var "x")) ($#r1_orders_2 :::"<="::: ) (Set (Var "y")))) "holds" (Bool (Set "f" ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_orders_2 :::"<="::: ) (Set "f" ($#k3_funct_2 :::"."::: ) (Set (Var "y"))))); end; :: deftheorem defines :::"monotone"::: WAYBEL_1:def 2 : (Bool "for" (Set (Var "L1")) "," (Set (Var "L2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "L1")) "," (Set (Var "L2")) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v5_orders_3 :::"monotone"::: ) ) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L1")) "st" (Bool (Bool (Set (Var "x")) ($#r1_orders_2 :::"<="::: ) (Set (Var "y")))) "holds" (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_orders_2 :::"<="::: ) (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "y"))))) ")" ))); theorem :: WAYBEL_1:1 (Bool "for" (Set (Var "L")) "being" ($#v4_orders_2 :::"transitive"::: ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#v2_lattice3 :::"with_infima"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "x")) ($#r1_orders_2 :::"<="::: ) (Set (Var "y")))) "holds" (Bool (Set (Set (Var "x")) ($#k12_lattice3 :::""/\""::: ) (Set (Var "z"))) ($#r1_orders_2 :::"<="::: ) (Set (Set (Var "y")) ($#k12_lattice3 :::""/\""::: ) (Set (Var "z")))))) ; theorem :: WAYBEL_1:2 (Bool "for" (Set (Var "L")) "being" ($#v4_orders_2 :::"transitive"::: ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#v1_lattice3 :::"with_suprema"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "x")) ($#r1_orders_2 :::"<="::: ) (Set (Var "y")))) "holds" (Bool (Set (Set (Var "x")) ($#k13_lattice3 :::""\/""::: ) (Set (Var "z"))) ($#r1_orders_2 :::"<="::: ) (Set (Set (Var "y")) ($#k13_lattice3 :::""\/""::: ) (Set (Var "z")))))) ; theorem :: WAYBEL_1:3 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#v1_yellow_0 :::"lower-bounded"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "L")) "is" ($#v2_lattice3 :::"with_infima"::: ) )) "implies" (Bool (Set (Set "(" ($#k3_yellow_0 :::"Bottom"::: ) (Set (Var "L")) ")" ) ($#k11_lattice3 :::""/\""::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k3_yellow_0 :::"Bottom"::: ) (Set (Var "L")))) ")" & "(" (Bool (Bool (Set (Var "L")) "is" ($#v1_lattice3 :::"with_suprema"::: ) ) & (Bool (Set (Var "L")) "is" ($#v3_orders_2 :::"reflexive"::: ) ) & (Bool (Set (Var "L")) "is" ($#v4_orders_2 :::"transitive"::: ) )) "implies" (Bool (Set (Set "(" ($#k3_yellow_0 :::"Bottom"::: ) (Set (Var "L")) ")" ) ($#k10_lattice3 :::""\/""::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Var "x"))) ")" ")" ))) ; theorem :: WAYBEL_1:4 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#v2_yellow_0 :::"upper-bounded"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "L")) "is" ($#v2_lattice3 :::"with_infima"::: ) ) & (Bool (Set (Var "L")) "is" ($#v4_orders_2 :::"transitive"::: ) ) & (Bool (Set (Var "L")) "is" ($#v3_orders_2 :::"reflexive"::: ) )) "implies" (Bool (Set (Set "(" ($#k4_yellow_0 :::"Top"::: ) (Set (Var "L")) ")" ) ($#k11_lattice3 :::""/\""::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Var "x"))) ")" & "(" (Bool (Bool (Set (Var "L")) "is" ($#v1_lattice3 :::"with_suprema"::: ) )) "implies" (Bool (Set (Set "(" ($#k4_yellow_0 :::"Top"::: ) (Set (Var "L")) ")" ) ($#k10_lattice3 :::""\/""::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k4_yellow_0 :::"Top"::: ) (Set (Var "L")))) ")" ")" ))) ; definitionlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) ; attr "L" is :::"distributive"::: means :: WAYBEL_1:def 3 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" "L" "holds" (Bool (Set (Set (Var "x")) ($#k11_lattice3 :::""/\""::: ) (Set "(" (Set (Var "y")) ($#k10_lattice3 :::""\/""::: ) (Set (Var "z")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "x")) ($#k11_lattice3 :::""/\""::: ) (Set (Var "y")) ")" ) ($#k10_lattice3 :::""\/""::: ) (Set "(" (Set (Var "x")) ($#k11_lattice3 :::""/\""::: ) (Set (Var "z")) ")" )))); end; :: deftheorem defines :::"distributive"::: WAYBEL_1:def 3 : (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) "holds" (Bool "(" (Bool (Set (Var "L")) "is" ($#v2_waybel_1 :::"distributive"::: ) ) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set (Var "x")) ($#k11_lattice3 :::""/\""::: ) (Set "(" (Set (Var "y")) ($#k10_lattice3 :::""\/""::: ) (Set (Var "z")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "x")) ($#k11_lattice3 :::""/\""::: ) (Set (Var "y")) ")" ) ($#k10_lattice3 :::""\/""::: ) (Set "(" (Set (Var "x")) ($#k11_lattice3 :::""/\""::: ) (Set (Var "z")) ")" )))) ")" )); theorem :: WAYBEL_1:5 (Bool "for" (Set (Var "L")) "being" ($#l1_orders_2 :::"LATTICE":::) "holds" (Bool "(" (Bool (Set (Var "L")) "is" ($#v2_waybel_1 :::"distributive"::: ) ) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set (Var "x")) ($#k13_lattice3 :::""\/""::: ) (Set "(" (Set (Var "y")) ($#k12_lattice3 :::""/\""::: ) (Set (Var "z")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "x")) ($#k13_lattice3 :::""\/""::: ) (Set (Var "y")) ")" ) ($#k12_lattice3 :::""/\""::: ) (Set "(" (Set (Var "x")) ($#k13_lattice3 :::""\/""::: ) (Set (Var "z")) ")" )))) ")" )) ; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k3_yellow_1 :::"BoolePoset"::: ) "X") -> ($#v2_waybel_1 :::"distributive"::: ) ; end; definitionlet "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) ; let "X" be ($#m1_hidden :::"set"::: ) ; pred :::"ex_min_of"::: "X" "," "S" means :: WAYBEL_1:def 4 (Bool "(" (Bool ($#r2_yellow_0 :::"ex_inf_of"::: ) "X" "," "S") & (Bool (Set ($#k2_yellow_0 :::""/\""::: ) "(" "X" "," "S" ")" ) ($#r2_hidden :::"in"::: ) "X") ")" ); pred :::"ex_max_of"::: "X" "," "S" means :: WAYBEL_1:def 5 (Bool "(" (Bool ($#r1_yellow_0 :::"ex_sup_of"::: ) "X" "," "S") & (Bool (Set ($#k1_yellow_0 :::""\/""::: ) "(" "X" "," "S" ")" ) ($#r2_hidden :::"in"::: ) "X") ")" ); end; :: deftheorem defines :::"ex_min_of"::: WAYBEL_1:def 4 : (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool ($#r1_waybel_1 :::"ex_min_of"::: ) (Set (Var "X")) "," (Set (Var "S"))) "iff" (Bool "(" (Bool ($#r2_yellow_0 :::"ex_inf_of"::: ) (Set (Var "X")) "," (Set (Var "S"))) & (Bool (Set ($#k2_yellow_0 :::""/\""::: ) "(" (Set (Var "X")) "," (Set (Var "S")) ")" ) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) ")" ) ")" ))); :: deftheorem defines :::"ex_max_of"::: WAYBEL_1:def 5 : (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool ($#r2_waybel_1 :::"ex_max_of"::: ) (Set (Var "X")) "," (Set (Var "S"))) "iff" (Bool "(" (Bool ($#r1_yellow_0 :::"ex_sup_of"::: ) (Set (Var "X")) "," (Set (Var "S"))) & (Bool (Set ($#k1_yellow_0 :::""\/""::: ) "(" (Set (Var "X")) "," (Set (Var "S")) ")" ) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) ")" ) ")" ))); notationlet "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) ; let "X" be ($#m1_hidden :::"set"::: ) ; synonym "X" :::"has_the_min_in"::: "S" for :::"ex_min_of"::: "X" "," "S"; synonym "X" :::"has_the_max_in"::: "S" for :::"ex_max_of"::: "X" "," "S"; end; definitionlet "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) ; let "s" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "S")); let "X" be ($#m1_hidden :::"set"::: ) ; pred "s" :::"is_minimum_of"::: "X" means :: WAYBEL_1:def 6 (Bool "(" (Bool ($#r2_yellow_0 :::"ex_inf_of"::: ) "X" "," "S") & (Bool "s" ($#r1_hidden :::"="::: ) (Set ($#k2_yellow_0 :::""/\""::: ) "(" "X" "," "S" ")" )) & (Bool (Set ($#k2_yellow_0 :::""/\""::: ) "(" "X" "," "S" ")" ) ($#r2_hidden :::"in"::: ) "X") ")" ); pred "s" :::"is_maximum_of"::: "X" means :: WAYBEL_1:def 7 (Bool "(" (Bool ($#r1_yellow_0 :::"ex_sup_of"::: ) "X" "," "S") & (Bool "s" ($#r1_hidden :::"="::: ) (Set ($#k1_yellow_0 :::""\/""::: ) "(" "X" "," "S" ")" )) & (Bool (Set ($#k1_yellow_0 :::""\/""::: ) "(" "X" "," "S" ")" ) ($#r2_hidden :::"in"::: ) "X") ")" ); end; :: deftheorem defines :::"is_minimum_of"::: WAYBEL_1:def 6 : (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "s")) ($#r3_waybel_1 :::"is_minimum_of"::: ) (Set (Var "X"))) "iff" (Bool "(" (Bool ($#r2_yellow_0 :::"ex_inf_of"::: ) (Set (Var "X")) "," (Set (Var "S"))) & (Bool (Set (Var "s")) ($#r1_hidden :::"="::: ) (Set ($#k2_yellow_0 :::""/\""::: ) "(" (Set (Var "X")) "," (Set (Var "S")) ")" )) & (Bool (Set ($#k2_yellow_0 :::""/\""::: ) "(" (Set (Var "X")) "," (Set (Var "S")) ")" ) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) ")" ) ")" )))); :: deftheorem defines :::"is_maximum_of"::: WAYBEL_1:def 7 : (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "s")) ($#r4_waybel_1 :::"is_maximum_of"::: ) (Set (Var "X"))) "iff" (Bool "(" (Bool ($#r1_yellow_0 :::"ex_sup_of"::: ) (Set (Var "X")) "," (Set (Var "S"))) & (Bool (Set (Var "s")) ($#r1_hidden :::"="::: ) (Set ($#k1_yellow_0 :::""\/""::: ) "(" (Set (Var "X")) "," (Set (Var "S")) ")" )) & (Bool (Set ($#k1_yellow_0 :::""\/""::: ) "(" (Set (Var "X")) "," (Set (Var "S")) ")" ) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) ")" ) ")" )))); registrationlet "L" be ($#l1_orders_2 :::"RelStr"::: ) ; cluster (Set ($#k3_struct_0 :::"id"::: ) "L") -> ($#v23_waybel_0 :::"isomorphic"::: ) ; end; definitionlet "L1", "L2" be ($#l1_orders_2 :::"RelStr"::: ) ; pred "L1" "," "L2" :::"are_isomorphic"::: means :: WAYBEL_1:def 8 (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" "L1" "," "L2" "st" (Bool (Set (Var "f")) "is" ($#v23_waybel_0 :::"isomorphic"::: ) )); reflexivity (Bool "for" (Set (Var "L1")) "being" ($#l1_orders_2 :::"RelStr"::: ) (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "L1")) "," (Set (Var "L1")) "st" (Bool (Set (Var "f")) "is" ($#v23_waybel_0 :::"isomorphic"::: ) ))) ; end; :: deftheorem defines :::"are_isomorphic"::: WAYBEL_1:def 8 : (Bool "for" (Set (Var "L1")) "," (Set (Var "L2")) "being" ($#l1_orders_2 :::"RelStr"::: ) "holds" (Bool "(" (Bool (Set (Var "L1")) "," (Set (Var "L2")) ($#r5_waybel_1 :::"are_isomorphic"::: ) ) "iff" (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "L1")) "," (Set (Var "L2")) "st" (Bool (Set (Var "f")) "is" ($#v23_waybel_0 :::"isomorphic"::: ) )) ")" )); theorem :: WAYBEL_1:6 (Bool "for" (Set (Var "L1")) "," (Set (Var "L2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) "st" (Bool (Bool (Set (Var "L1")) "," (Set (Var "L2")) ($#r5_waybel_1 :::"are_isomorphic"::: ) )) "holds" (Bool (Set (Var "L2")) "," (Set (Var "L1")) ($#r5_waybel_1 :::"are_isomorphic"::: ) )) ; theorem :: WAYBEL_1:7 (Bool "for" (Set (Var "L1")) "," (Set (Var "L2")) "," (Set (Var "L3")) "being" ($#l1_orders_2 :::"RelStr"::: ) "st" (Bool (Bool (Set (Var "L1")) "," (Set (Var "L2")) ($#r5_waybel_1 :::"are_isomorphic"::: ) ) & (Bool (Set (Var "L2")) "," (Set (Var "L3")) ($#r5_waybel_1 :::"are_isomorphic"::: ) )) "holds" (Bool (Set (Var "L1")) "," (Set (Var "L3")) ($#r5_waybel_1 :::"are_isomorphic"::: ) )) ; begin definitionlet "S", "T" be ($#l1_orders_2 :::"RelStr"::: ) ; mode :::"Connection"::: "of" "S" "," "T" -> ($#m1_hidden :::"set"::: ) means :: WAYBEL_1:def 9 (Bool "ex" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" "S" "," "T"(Bool "ex" (Set (Var "d")) "being" ($#m1_subset_1 :::"Function":::) "of" "T" "," "S" "st" (Bool it ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "g")) "," (Set (Var "d")) ($#k4_tarski :::"]"::: ) )))); end; :: deftheorem defines :::"Connection"::: WAYBEL_1:def 9 : (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "b3")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "b3")) "is" ($#m1_waybel_1 :::"Connection"::: ) "of" (Set (Var "S")) "," (Set (Var "T"))) "iff" (Bool "ex" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set (Var "T"))(Bool "ex" (Set (Var "d")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "T")) "," (Set (Var "S")) "st" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "g")) "," (Set (Var "d")) ($#k4_tarski :::"]"::: ) )))) ")" ))); definitionlet "S", "T" be ($#l1_orders_2 :::"RelStr"::: ) ; let "g" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "S")) "," (Set (Const "T")); let "d" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "T")) "," (Set (Const "S")); :: original: :::"["::: redefine func :::"[":::"g" "," "d":::"]"::: -> ($#m1_waybel_1 :::"Connection"::: ) "of" "S" "," "T"; end; definitionlet "S", "T" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) ; let "gc" be ($#m1_waybel_1 :::"Connection"::: ) "of" (Set (Const "S")) "," (Set (Const "T")); attr "gc" is :::"Galois"::: means :: WAYBEL_1:def 10 (Bool "ex" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" "S" "," "T"(Bool "ex" (Set (Var "d")) "being" ($#m1_subset_1 :::"Function":::) "of" "T" "," "S" "st" (Bool "(" (Bool "gc" ($#r1_hidden :::"="::: ) (Set ($#k1_waybel_1 :::"["::: ) (Set (Var "g")) "," (Set (Var "d")) ($#k1_waybel_1 :::"]"::: ) )) & (Bool (Set (Var "g")) "is" ($#v5_orders_3 :::"monotone"::: ) ) & (Bool (Set (Var "d")) "is" ($#v5_orders_3 :::"monotone"::: ) ) & (Bool "(" "for" (Set (Var "t")) "being" ($#m1_subset_1 :::"Element":::) "of" "T" (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"Element":::) "of" "S" "holds" (Bool "(" (Bool (Set (Var "t")) ($#r1_orders_2 :::"<="::: ) (Set (Set (Var "g")) ($#k3_funct_2 :::"."::: ) (Set (Var "s")))) "iff" (Bool (Set (Set (Var "d")) ($#k3_funct_2 :::"."::: ) (Set (Var "t"))) ($#r1_orders_2 :::"<="::: ) (Set (Var "s"))) ")" )) ")" ) ")" ))); end; :: deftheorem defines :::"Galois"::: WAYBEL_1:def 10 : (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "gc")) "being" ($#m1_waybel_1 :::"Connection"::: ) "of" (Set (Var "S")) "," (Set (Var "T")) "holds" (Bool "(" (Bool (Set (Var "gc")) "is" ($#v3_waybel_1 :::"Galois"::: ) ) "iff" (Bool "ex" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set (Var "T"))(Bool "ex" (Set (Var "d")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "T")) "," (Set (Var "S")) "st" (Bool "(" (Bool (Set (Var "gc")) ($#r1_hidden :::"="::: ) (Set ($#k1_waybel_1 :::"["::: ) (Set (Var "g")) "," (Set (Var "d")) ($#k1_waybel_1 :::"]"::: ) )) & (Bool (Set (Var "g")) "is" ($#v5_orders_3 :::"monotone"::: ) ) & (Bool (Set (Var "d")) "is" ($#v5_orders_3 :::"monotone"::: ) ) & (Bool "(" "for" (Set (Var "t")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) "holds" (Bool "(" (Bool (Set (Var "t")) ($#r1_orders_2 :::"<="::: ) (Set (Set (Var "g")) ($#k3_funct_2 :::"."::: ) (Set (Var "s")))) "iff" (Bool (Set (Set (Var "d")) ($#k3_funct_2 :::"."::: ) (Set (Var "t"))) ($#r1_orders_2 :::"<="::: ) (Set (Var "s"))) ")" )) ")" ) ")" ))) ")" ))); theorem :: WAYBEL_1:8 (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set (Var "T")) (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "T")) "," (Set (Var "S")) "holds" (Bool "(" (Bool (Set ($#k1_waybel_1 :::"["::: ) (Set (Var "g")) "," (Set (Var "d")) ($#k1_waybel_1 :::"]"::: ) ) "is" ($#v3_waybel_1 :::"Galois"::: ) ) "iff" (Bool "(" (Bool (Set (Var "g")) "is" ($#v5_orders_3 :::"monotone"::: ) ) & (Bool (Set (Var "d")) "is" ($#v5_orders_3 :::"monotone"::: ) ) & (Bool "(" "for" (Set (Var "t")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) "holds" (Bool "(" (Bool (Set (Var "t")) ($#r3_orders_2 :::"<="::: ) (Set (Set (Var "g")) ($#k3_funct_2 :::"."::: ) (Set (Var "s")))) "iff" (Bool (Set (Set (Var "d")) ($#k3_funct_2 :::"."::: ) (Set (Var "t"))) ($#r3_orders_2 :::"<="::: ) (Set (Var "s"))) ")" )) ")" ) ")" ) ")" )))) ; definitionlet "S", "T" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) ; let "g" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "S")) "," (Set (Const "T")); attr "g" is :::"upper_adjoint"::: means :: WAYBEL_1:def 11 (Bool "ex" (Set (Var "d")) "being" ($#m1_subset_1 :::"Function":::) "of" "T" "," "S" "st" (Bool (Set ($#k1_waybel_1 :::"["::: ) "g" "," (Set (Var "d")) ($#k1_waybel_1 :::"]"::: ) ) "is" ($#v3_waybel_1 :::"Galois"::: ) )); end; :: deftheorem defines :::"upper_adjoint"::: WAYBEL_1:def 11 : (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set (Var "T")) "holds" (Bool "(" (Bool (Set (Var "g")) "is" ($#v4_waybel_1 :::"upper_adjoint"::: ) ) "iff" (Bool "ex" (Set (Var "d")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "T")) "," (Set (Var "S")) "st" (Bool (Set ($#k1_waybel_1 :::"["::: ) (Set (Var "g")) "," (Set (Var "d")) ($#k1_waybel_1 :::"]"::: ) ) "is" ($#v3_waybel_1 :::"Galois"::: ) )) ")" ))); definitionlet "S", "T" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) ; let "d" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "T")) "," (Set (Const "S")); attr "d" is :::"lower_adjoint"::: means :: WAYBEL_1:def 12 (Bool "ex" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" "S" "," "T" "st" (Bool (Set ($#k1_waybel_1 :::"["::: ) (Set (Var "g")) "," "d" ($#k1_waybel_1 :::"]"::: ) ) "is" ($#v3_waybel_1 :::"Galois"::: ) )); end; :: deftheorem defines :::"lower_adjoint"::: WAYBEL_1:def 12 : (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "T")) "," (Set (Var "S")) "holds" (Bool "(" (Bool (Set (Var "d")) "is" ($#v5_waybel_1 :::"lower_adjoint"::: ) ) "iff" (Bool "ex" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set (Var "T")) "st" (Bool (Set ($#k1_waybel_1 :::"["::: ) (Set (Var "g")) "," (Set (Var "d")) ($#k1_waybel_1 :::"]"::: ) ) "is" ($#v3_waybel_1 :::"Galois"::: ) )) ")" ))); theorem :: WAYBEL_1:9 (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set (Var "T")) (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "T")) "," (Set (Var "S")) "st" (Bool (Bool (Set ($#k1_waybel_1 :::"["::: ) (Set (Var "g")) "," (Set (Var "d")) ($#k1_waybel_1 :::"]"::: ) ) "is" ($#v3_waybel_1 :::"Galois"::: ) )) "holds" (Bool "(" (Bool (Set (Var "g")) "is" ($#v4_waybel_1 :::"upper_adjoint"::: ) ) & (Bool (Set (Var "d")) "is" ($#v5_waybel_1 :::"lower_adjoint"::: ) ) ")" )))) ; theorem :: WAYBEL_1:10 (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set (Var "T")) (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "T")) "," (Set (Var "S")) "holds" (Bool "(" (Bool (Set ($#k1_waybel_1 :::"["::: ) (Set (Var "g")) "," (Set (Var "d")) ($#k1_waybel_1 :::"]"::: ) ) "is" ($#v3_waybel_1 :::"Galois"::: ) ) "iff" (Bool "(" (Bool (Set (Var "g")) "is" ($#v5_orders_3 :::"monotone"::: ) ) & (Bool "(" "for" (Set (Var "t")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "T")) "holds" (Bool (Set (Set (Var "d")) ($#k3_funct_2 :::"."::: ) (Set (Var "t"))) ($#r3_waybel_1 :::"is_minimum_of"::: ) (Set (Set (Var "g")) ($#k8_relset_1 :::"""::: ) (Set "(" ($#k6_waybel_0 :::"uparrow"::: ) (Set (Var "t")) ")" ))) ")" ) ")" ) ")" )))) ; theorem :: WAYBEL_1:11 (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set (Var "T")) (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "T")) "," (Set (Var "S")) "holds" (Bool "(" (Bool (Set ($#k1_waybel_1 :::"["::: ) (Set (Var "g")) "," (Set (Var "d")) ($#k1_waybel_1 :::"]"::: ) ) "is" ($#v3_waybel_1 :::"Galois"::: ) ) "iff" (Bool "(" (Bool (Set (Var "d")) "is" ($#v5_orders_3 :::"monotone"::: ) ) & (Bool "(" "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) "holds" (Bool (Set (Set (Var "g")) ($#k3_funct_2 :::"."::: ) (Set (Var "s"))) ($#r4_waybel_1 :::"is_maximum_of"::: ) (Set (Set (Var "d")) ($#k8_relset_1 :::"""::: ) (Set "(" ($#k5_waybel_0 :::"downarrow"::: ) (Set (Var "s")) ")" ))) ")" ) ")" ) ")" )))) ; theorem :: WAYBEL_1:12 (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set (Var "T")) "st" (Bool (Bool (Set (Var "g")) "is" ($#v4_waybel_1 :::"upper_adjoint"::: ) )) "holds" (Bool (Set (Var "g")) "is" ($#v17_waybel_0 :::"infs-preserving"::: ) ))) ; registrationlet "S", "T" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"Poset":::); cluster ($#v1_funct_1 :::"Function-like"::: ) ($#v1_funct_2 :::"quasi_total"::: ) ($#v4_waybel_1 :::"upper_adjoint"::: ) -> ($#v17_waybel_0 :::"infs-preserving"::: ) for bbbadM1_SUBSET_1((Set ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "S") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "T") ($#k2_zfmisc_1 :::":]"::: ) ))); end; theorem :: WAYBEL_1:13 (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "T")) "," (Set (Var "S")) "st" (Bool (Bool (Set (Var "d")) "is" ($#v5_waybel_1 :::"lower_adjoint"::: ) )) "holds" (Bool (Set (Var "d")) "is" ($#v18_waybel_0 :::"sups-preserving"::: ) ))) ; registrationlet "S", "T" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"Poset":::); cluster ($#v1_funct_1 :::"Function-like"::: ) ($#v1_funct_2 :::"quasi_total"::: ) ($#v5_waybel_1 :::"lower_adjoint"::: ) -> ($#v18_waybel_0 :::"sups-preserving"::: ) for bbbadM1_SUBSET_1((Set ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "S") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "T") ($#k2_zfmisc_1 :::":]"::: ) ))); end; theorem :: WAYBEL_1:14 (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set (Var "T")) "st" (Bool (Bool (Set (Var "S")) "is" ($#v3_lattice3 :::"complete"::: ) ) & (Bool (Set (Var "g")) "is" ($#v17_waybel_0 :::"infs-preserving"::: ) )) "holds" (Bool "ex" (Set (Var "d")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "T")) "," (Set (Var "S")) "st" (Bool "(" (Bool (Set ($#k1_waybel_1 :::"["::: ) (Set (Var "g")) "," (Set (Var "d")) ($#k1_waybel_1 :::"]"::: ) ) "is" ($#v3_waybel_1 :::"Galois"::: ) ) & (Bool "(" "for" (Set (Var "t")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "T")) "holds" (Bool (Set (Set (Var "d")) ($#k3_funct_2 :::"."::: ) (Set (Var "t"))) ($#r3_waybel_1 :::"is_minimum_of"::: ) (Set (Set (Var "g")) ($#k8_relset_1 :::"""::: ) (Set "(" ($#k6_waybel_0 :::"uparrow"::: ) (Set (Var "t")) ")" ))) ")" ) ")" )))) ; theorem :: WAYBEL_1:15 (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "T")) "," (Set (Var "S")) "st" (Bool (Bool (Set (Var "T")) "is" ($#v3_lattice3 :::"complete"::: ) ) & (Bool (Set (Var "d")) "is" ($#v18_waybel_0 :::"sups-preserving"::: ) )) "holds" (Bool "ex" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set (Var "T")) "st" (Bool "(" (Bool (Set ($#k1_waybel_1 :::"["::: ) (Set (Var "g")) "," (Set (Var "d")) ($#k1_waybel_1 :::"]"::: ) ) "is" ($#v3_waybel_1 :::"Galois"::: ) ) & (Bool "(" "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) "holds" (Bool (Set (Set (Var "g")) ($#k3_funct_2 :::"."::: ) (Set (Var "s"))) ($#r4_waybel_1 :::"is_maximum_of"::: ) (Set (Set (Var "d")) ($#k8_relset_1 :::"""::: ) (Set "(" ($#k5_waybel_0 :::"downarrow"::: ) (Set (Var "s")) ")" ))) ")" ) ")" )))) ; theorem :: WAYBEL_1:16 (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set (Var "T")) "st" (Bool (Bool (Set (Var "S")) "is" ($#v3_lattice3 :::"complete"::: ) )) "holds" (Bool "(" (Bool (Set (Var "g")) "is" ($#v17_waybel_0 :::"infs-preserving"::: ) ) "iff" (Bool "(" (Bool (Set (Var "g")) "is" ($#v5_orders_3 :::"monotone"::: ) ) & (Bool (Set (Var "g")) "is" ($#v4_waybel_1 :::"upper_adjoint"::: ) ) ")" ) ")" ))) ; theorem :: WAYBEL_1:17 (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "T")) "," (Set (Var "S")) "st" (Bool (Bool (Set (Var "T")) "is" ($#v3_lattice3 :::"complete"::: ) )) "holds" (Bool "(" (Bool (Set (Var "d")) "is" ($#v18_waybel_0 :::"sups-preserving"::: ) ) "iff" (Bool "(" (Bool (Set (Var "d")) "is" ($#v5_orders_3 :::"monotone"::: ) ) & (Bool (Set (Var "d")) "is" ($#v5_waybel_1 :::"lower_adjoint"::: ) ) ")" ) ")" ))) ; theorem :: WAYBEL_1:18 (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set (Var "T")) (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "T")) "," (Set (Var "S")) "st" (Bool (Bool (Set ($#k1_waybel_1 :::"["::: ) (Set (Var "g")) "," (Set (Var "d")) ($#k1_waybel_1 :::"]"::: ) ) "is" ($#v3_waybel_1 :::"Galois"::: ) )) "holds" (Bool "(" (Bool (Set (Set (Var "d")) ($#k1_partfun1 :::"*"::: ) (Set (Var "g"))) ($#r1_yellow_2 :::"<="::: ) (Set ($#k3_struct_0 :::"id"::: ) (Set (Var "S")))) & (Bool (Set ($#k3_struct_0 :::"id"::: ) (Set (Var "T"))) ($#r1_yellow_2 :::"<="::: ) (Set (Set (Var "g")) ($#k1_partfun1 :::"*"::: ) (Set (Var "d")))) ")" )))) ; theorem :: WAYBEL_1:19 (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set (Var "T")) (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "T")) "," (Set (Var "S")) "st" (Bool (Bool (Set (Var "g")) "is" ($#v5_orders_3 :::"monotone"::: ) ) & (Bool (Set (Var "d")) "is" ($#v5_orders_3 :::"monotone"::: ) ) & (Bool (Set (Set (Var "d")) ($#k1_partfun1 :::"*"::: ) (Set (Var "g"))) ($#r1_yellow_2 :::"<="::: ) (Set ($#k3_struct_0 :::"id"::: ) (Set (Var "S")))) & (Bool (Set ($#k3_struct_0 :::"id"::: ) (Set (Var "T"))) ($#r1_yellow_2 :::"<="::: ) (Set (Set (Var "g")) ($#k1_partfun1 :::"*"::: ) (Set (Var "d"))))) "holds" (Bool (Set ($#k1_waybel_1 :::"["::: ) (Set (Var "g")) "," (Set (Var "d")) ($#k1_waybel_1 :::"]"::: ) ) "is" ($#v3_waybel_1 :::"Galois"::: ) )))) ; theorem :: WAYBEL_1:20 (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set (Var "T")) (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "T")) "," (Set (Var "S")) "st" (Bool (Bool (Set (Var "g")) "is" ($#v5_orders_3 :::"monotone"::: ) ) & (Bool (Set (Var "d")) "is" ($#v5_orders_3 :::"monotone"::: ) ) & (Bool (Set (Set (Var "d")) ($#k1_partfun1 :::"*"::: ) (Set (Var "g"))) ($#r1_yellow_2 :::"<="::: ) (Set ($#k3_struct_0 :::"id"::: ) (Set (Var "S")))) & (Bool (Set ($#k3_struct_0 :::"id"::: ) (Set (Var "T"))) ($#r1_yellow_2 :::"<="::: ) (Set (Set (Var "g")) ($#k1_partfun1 :::"*"::: ) (Set (Var "d"))))) "holds" (Bool "(" (Bool (Set (Var "d")) ($#r2_funct_2 :::"="::: ) (Set (Set "(" (Set (Var "d")) ($#k1_partfun1 :::"*"::: ) (Set (Var "g")) ")" ) ($#k1_partfun1 :::"*"::: ) (Set (Var "d")))) & (Bool (Set (Var "g")) ($#r2_funct_2 :::"="::: ) (Set (Set "(" (Set (Var "g")) ($#k1_partfun1 :::"*"::: ) (Set (Var "d")) ")" ) ($#k1_partfun1 :::"*"::: ) (Set (Var "g")))) ")" )))) ; theorem :: WAYBEL_1:21 (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set (Var "T")) (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "T")) "," (Set (Var "S")) "st" (Bool (Bool (Set (Var "g")) ($#r2_funct_2 :::"="::: ) (Set (Set "(" (Set (Var "g")) ($#k1_partfun1 :::"*"::: ) (Set (Var "d")) ")" ) ($#k1_partfun1 :::"*"::: ) (Set (Var "g"))))) "holds" (Bool (Set (Set (Var "g")) ($#k1_partfun1 :::"*"::: ) (Set (Var "d"))) "is" ($#v11_quantal1 :::"idempotent"::: ) )))) ; theorem :: WAYBEL_1:22 (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set (Var "T")) (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "T")) "," (Set (Var "S")) "st" (Bool (Bool (Set ($#k1_waybel_1 :::"["::: ) (Set (Var "g")) "," (Set (Var "d")) ($#k1_waybel_1 :::"]"::: ) ) "is" ($#v3_waybel_1 :::"Galois"::: ) ) & (Bool (Set (Var "g")) "is" ($#v2_funct_2 :::"onto"::: ) )) "holds" (Bool "for" (Set (Var "t")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "T")) "holds" (Bool (Set (Set (Var "d")) ($#k3_funct_2 :::"."::: ) (Set (Var "t"))) ($#r3_waybel_1 :::"is_minimum_of"::: ) (Set (Set (Var "g")) ($#k8_relset_1 :::"""::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "t")) ($#k6_domain_1 :::"}"::: ) ))))))) ; theorem :: WAYBEL_1:23 (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set (Var "T")) (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "T")) "," (Set (Var "S")) "st" (Bool (Bool "(" "for" (Set (Var "t")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "T")) "holds" (Bool (Set (Set (Var "d")) ($#k3_funct_2 :::"."::: ) (Set (Var "t"))) ($#r3_waybel_1 :::"is_minimum_of"::: ) (Set (Set (Var "g")) ($#k8_relset_1 :::"""::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "t")) ($#k6_domain_1 :::"}"::: ) ))) ")" )) "holds" (Bool (Set (Set (Var "g")) ($#k1_partfun1 :::"*"::: ) (Set (Var "d"))) ($#r2_funct_2 :::"="::: ) (Set ($#k3_struct_0 :::"id"::: ) (Set (Var "T"))))))) ; theorem :: WAYBEL_1:24 (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set (Var "T")) (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "T")) "," (Set (Var "S")) "st" (Bool (Bool (Set ($#k1_waybel_1 :::"["::: ) (Set (Var "g")) "," (Set (Var "d")) ($#k1_waybel_1 :::"]"::: ) ) "is" ($#v3_waybel_1 :::"Galois"::: ) )) "holds" (Bool "(" (Bool (Set (Var "g")) "is" ($#v2_funct_2 :::"onto"::: ) ) "iff" (Bool (Set (Var "d")) "is" bbbadV2_FUNCT_1()) ")" )))) ; theorem :: WAYBEL_1:25 (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set (Var "T")) (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "T")) "," (Set (Var "S")) "st" (Bool (Bool (Set ($#k1_waybel_1 :::"["::: ) (Set (Var "g")) "," (Set (Var "d")) ($#k1_waybel_1 :::"]"::: ) ) "is" ($#v3_waybel_1 :::"Galois"::: ) ) & (Bool (Set (Var "d")) "is" ($#v2_funct_2 :::"onto"::: ) )) "holds" (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) "holds" (Bool (Set (Set (Var "g")) ($#k3_funct_2 :::"."::: ) (Set (Var "s"))) ($#r4_waybel_1 :::"is_maximum_of"::: ) (Set (Set (Var "d")) ($#k8_relset_1 :::"""::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "s")) ($#k6_domain_1 :::"}"::: ) ))))))) ; theorem :: WAYBEL_1:26 (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set (Var "T")) (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "T")) "," (Set (Var "S")) "st" (Bool (Bool "(" "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) "holds" (Bool (Set (Set (Var "g")) ($#k3_funct_2 :::"."::: ) (Set (Var "s"))) ($#r4_waybel_1 :::"is_maximum_of"::: ) (Set (Set (Var "d")) ($#k8_relset_1 :::"""::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "s")) ($#k6_domain_1 :::"}"::: ) ))) ")" )) "holds" (Bool (Set (Set (Var "d")) ($#k1_partfun1 :::"*"::: ) (Set (Var "g"))) ($#r2_funct_2 :::"="::: ) (Set ($#k3_struct_0 :::"id"::: ) (Set (Var "S"))))))) ; theorem :: WAYBEL_1:27 (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set (Var "T")) (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "T")) "," (Set (Var "S")) "st" (Bool (Bool (Set ($#k1_waybel_1 :::"["::: ) (Set (Var "g")) "," (Set (Var "d")) ($#k1_waybel_1 :::"]"::: ) ) "is" ($#v3_waybel_1 :::"Galois"::: ) )) "holds" (Bool "(" (Bool (Set (Var "g")) "is" bbbadV2_FUNCT_1()) "iff" (Bool (Set (Var "d")) "is" ($#v2_funct_2 :::"onto"::: ) ) ")" )))) ; definitionlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) ; let "p" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "L")) "," (Set (Const "L")); attr "p" is :::"projection"::: means :: WAYBEL_1:def 13 (Bool "(" (Bool "p" "is" ($#v11_quantal1 :::"idempotent"::: ) ) & (Bool "p" "is" ($#v5_orders_3 :::"monotone"::: ) ) ")" ); end; :: deftheorem defines :::"projection"::: WAYBEL_1:def 13 : (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "L")) "," (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "p")) "is" ($#v6_waybel_1 :::"projection"::: ) ) "iff" (Bool "(" (Bool (Set (Var "p")) "is" ($#v11_quantal1 :::"idempotent"::: ) ) & (Bool (Set (Var "p")) "is" ($#v5_orders_3 :::"monotone"::: ) ) ")" ) ")" ))); registrationlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) ; cluster (Set ($#k3_struct_0 :::"id"::: ) "L") -> ($#v6_waybel_1 :::"projection"::: ) ; end; registrationlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) ; cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) bbbadV1_RELAT_1() bbbadV4_RELAT_1((Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "L")) bbbadV5_RELAT_1((Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "L")) ($#v1_funct_1 :::"Function-like"::: ) bbbadV1_PARTFUN1((Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "L")) ($#v1_funct_2 :::"quasi_total"::: ) ($#v6_waybel_1 :::"projection"::: ) for bbbadM1_SUBSET_1((Set ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "L") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "L") ($#k2_zfmisc_1 :::":]"::: ) ))); end; definitionlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) ; let "c" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "L")) "," (Set (Const "L")); attr "c" is :::"closure"::: means :: WAYBEL_1:def 14 (Bool "(" (Bool "c" "is" ($#v6_waybel_1 :::"projection"::: ) ) & (Bool (Set ($#k3_struct_0 :::"id"::: ) "L") ($#r1_yellow_2 :::"<="::: ) "c") ")" ); end; :: deftheorem defines :::"closure"::: WAYBEL_1:def 14 : (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "L")) "," (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "c")) "is" ($#v7_waybel_1 :::"closure"::: ) ) "iff" (Bool "(" (Bool (Set (Var "c")) "is" ($#v6_waybel_1 :::"projection"::: ) ) & (Bool (Set ($#k3_struct_0 :::"id"::: ) (Set (Var "L"))) ($#r1_yellow_2 :::"<="::: ) (Set (Var "c"))) ")" ) ")" ))); registrationlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) ; cluster ($#v1_funct_1 :::"Function-like"::: ) ($#v1_funct_2 :::"quasi_total"::: ) ($#v7_waybel_1 :::"closure"::: ) -> ($#v6_waybel_1 :::"projection"::: ) for bbbadM1_SUBSET_1((Set ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "L") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "L") ($#k2_zfmisc_1 :::":]"::: ) ))); end; registrationlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) bbbadV1_RELAT_1() bbbadV4_RELAT_1((Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "L")) bbbadV5_RELAT_1((Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "L")) ($#v1_funct_1 :::"Function-like"::: ) bbbadV1_PARTFUN1((Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "L")) ($#v1_funct_2 :::"quasi_total"::: ) ($#v7_waybel_1 :::"closure"::: ) for bbbadM1_SUBSET_1((Set ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "L") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "L") ($#k2_zfmisc_1 :::":]"::: ) ))); end; registrationlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; cluster (Set ($#k3_struct_0 :::"id"::: ) "L") -> ($#v7_waybel_1 :::"closure"::: ) ; end; definitionlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) ; let "k" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "L")) "," (Set (Const "L")); attr "k" is :::"kernel"::: means :: WAYBEL_1:def 15 (Bool "(" (Bool "k" "is" ($#v6_waybel_1 :::"projection"::: ) ) & (Bool "k" ($#r1_yellow_2 :::"<="::: ) (Set ($#k3_struct_0 :::"id"::: ) "L")) ")" ); end; :: deftheorem defines :::"kernel"::: WAYBEL_1:def 15 : (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "k")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "L")) "," (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "k")) "is" ($#v8_waybel_1 :::"kernel"::: ) ) "iff" (Bool "(" (Bool (Set (Var "k")) "is" ($#v6_waybel_1 :::"projection"::: ) ) & (Bool (Set (Var "k")) ($#r1_yellow_2 :::"<="::: ) (Set ($#k3_struct_0 :::"id"::: ) (Set (Var "L")))) ")" ) ")" ))); registrationlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) ; cluster ($#v1_funct_1 :::"Function-like"::: ) ($#v1_funct_2 :::"quasi_total"::: ) ($#v8_waybel_1 :::"kernel"::: ) -> ($#v6_waybel_1 :::"projection"::: ) for bbbadM1_SUBSET_1((Set ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "L") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "L") ($#k2_zfmisc_1 :::":]"::: ) ))); end; registrationlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) bbbadV1_RELAT_1() bbbadV4_RELAT_1((Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "L")) bbbadV5_RELAT_1((Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "L")) ($#v1_funct_1 :::"Function-like"::: ) bbbadV1_PARTFUN1((Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "L")) ($#v1_funct_2 :::"quasi_total"::: ) ($#v8_waybel_1 :::"kernel"::: ) for bbbadM1_SUBSET_1((Set ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "L") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "L") ($#k2_zfmisc_1 :::":]"::: ) ))); end; registrationlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; cluster (Set ($#k3_struct_0 :::"id"::: ) "L") -> ($#v8_waybel_1 :::"kernel"::: ) ; end; theorem :: WAYBEL_1:28 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "L")) "," (Set (Var "L")) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "c")) "is" ($#v7_waybel_1 :::"closure"::: ) ) & (Bool ($#r2_yellow_0 :::"ex_inf_of"::: ) (Set (Var "X")) "," (Set (Var "L"))) & (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "c"))))) "holds" (Bool (Set ($#k2_yellow_0 :::"inf"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "c")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k2_yellow_0 :::"inf"::: ) (Set (Var "X")) ")" )))))) ; theorem :: WAYBEL_1:29 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "k")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "L")) "," (Set (Var "L")) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "k")) "is" ($#v8_waybel_1 :::"kernel"::: ) ) & (Bool ($#r1_yellow_0 :::"ex_sup_of"::: ) (Set (Var "X")) "," (Set (Var "L"))) & (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "k"))))) "holds" (Bool (Set ($#k1_yellow_0 :::"sup"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "k")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k1_yellow_0 :::"sup"::: ) (Set (Var "X")) ")" )))))) ; definitionlet "L1", "L2" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) ; let "g" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "L1")) "," (Set (Const "L2")); func :::"corestr"::: "g" -> ($#m1_subset_1 :::"Function":::) "of" "L1" "," (Set "(" ($#k1_yellow_2 :::"Image"::: ) "g" ")" ) equals :: WAYBEL_1:def 16 (Set (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k1_yellow_2 :::"Image"::: ) "g" ")" )) ($#k6_relset_1 :::"|`"::: ) "g"); end; :: deftheorem defines :::"corestr"::: WAYBEL_1:def 16 : (Bool "for" (Set (Var "L1")) "," (Set (Var "L2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "L1")) "," (Set (Var "L2")) "holds" (Bool (Set ($#k2_waybel_1 :::"corestr"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k1_yellow_2 :::"Image"::: ) (Set (Var "g")) ")" )) ($#k6_relset_1 :::"|`"::: ) (Set (Var "g")))))); theorem :: WAYBEL_1:30 (Bool "for" (Set (Var "L1")) "," (Set (Var "L2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "L1")) "," (Set (Var "L2")) "holds" (Bool (Set ($#k2_waybel_1 :::"corestr"::: ) (Set (Var "g"))) ($#r1_funct_2 :::"="::: ) (Set (Var "g"))))) ; registrationlet "L1", "L2" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) ; let "g" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "L1")) "," (Set (Const "L2")); cluster (Set ($#k2_waybel_1 :::"corestr"::: ) "g") -> ($#v2_funct_2 :::"onto"::: ) ; end; theorem :: WAYBEL_1:31 (Bool "for" (Set (Var "L1")) "," (Set (Var "L2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "L1")) "," (Set (Var "L2")) "st" (Bool (Bool (Set (Var "g")) "is" ($#v5_orders_3 :::"monotone"::: ) )) "holds" (Bool (Set ($#k2_waybel_1 :::"corestr"::: ) (Set (Var "g"))) "is" ($#v5_orders_3 :::"monotone"::: ) ))) ; definitionlet "L1", "L2" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) ; let "g" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "L1")) "," (Set (Const "L2")); func :::"inclusion"::: "g" -> ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k1_yellow_2 :::"Image"::: ) "g" ")" ) "," "L2" equals :: WAYBEL_1:def 17 (Set ($#k3_struct_0 :::"id"::: ) (Set "(" ($#k1_yellow_2 :::"Image"::: ) "g" ")" )); end; :: deftheorem defines :::"inclusion"::: WAYBEL_1:def 17 : (Bool "for" (Set (Var "L1")) "," (Set (Var "L2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "L1")) "," (Set (Var "L2")) "holds" (Bool (Set ($#k3_waybel_1 :::"inclusion"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set ($#k3_struct_0 :::"id"::: ) (Set "(" ($#k1_yellow_2 :::"Image"::: ) (Set (Var "g")) ")" ))))); registrationlet "L1", "L2" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) ; let "g" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "L1")) "," (Set (Const "L2")); cluster (Set ($#k3_waybel_1 :::"inclusion"::: ) "g") -> bbbadV2_FUNCT_1() ($#v5_orders_3 :::"monotone"::: ) ; end; theorem :: WAYBEL_1:32 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "L")) "," (Set (Var "L")) "holds" (Bool (Set (Set "(" ($#k3_waybel_1 :::"inclusion"::: ) (Set (Var "f")) ")" ) ($#k1_partfun1 :::"*"::: ) (Set "(" ($#k2_waybel_1 :::"corestr"::: ) (Set (Var "f")) ")" )) ($#r2_funct_2 :::"="::: ) (Set (Var "f"))))) ; theorem :: WAYBEL_1:33 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "L")) "," (Set (Var "L")) "st" (Bool (Bool (Set (Var "f")) "is" ($#v11_quantal1 :::"idempotent"::: ) )) "holds" (Bool (Set (Set "(" ($#k2_waybel_1 :::"corestr"::: ) (Set (Var "f")) ")" ) ($#k1_partfun1 :::"*"::: ) (Set "(" ($#k3_waybel_1 :::"inclusion"::: ) (Set (Var "f")) ")" )) ($#r2_funct_2 :::"="::: ) (Set ($#k3_struct_0 :::"id"::: ) (Set "(" ($#k1_yellow_2 :::"Image"::: ) (Set (Var "f")) ")" ))))) ; theorem :: WAYBEL_1:34 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "L")) "," (Set (Var "L")) "st" (Bool (Bool (Set (Var "f")) "is" ($#v6_waybel_1 :::"projection"::: ) )) "holds" (Bool "ex" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"Poset":::)(Bool "ex" (Set (Var "q")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "L")) "," (Set (Var "T"))(Bool "ex" (Set (Var "i")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "T")) "," (Set (Var "L")) "st" (Bool "(" (Bool (Set (Var "q")) "is" ($#v5_orders_3 :::"monotone"::: ) ) & (Bool (Set (Var "q")) "is" ($#v2_funct_2 :::"onto"::: ) ) & (Bool (Set (Var "i")) "is" ($#v5_orders_3 :::"monotone"::: ) ) & (Bool (Set (Var "i")) "is" bbbadV2_FUNCT_1()) & (Bool (Set (Var "f")) ($#r2_funct_2 :::"="::: ) (Set (Set (Var "i")) ($#k1_partfun1 :::"*"::: ) (Set (Var "q")))) & (Bool (Set ($#k3_struct_0 :::"id"::: ) (Set (Var "T"))) ($#r2_funct_2 :::"="::: ) (Set (Set (Var "q")) ($#k1_partfun1 :::"*"::: ) (Set (Var "i")))) ")" )))))) ; theorem :: WAYBEL_1:35 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "L")) "," (Set (Var "L")) "st" (Bool (Bool "ex" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"Poset":::)(Bool "ex" (Set (Var "q")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "L")) "," (Set (Var "T"))(Bool "ex" (Set (Var "i")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "T")) "," (Set (Var "L")) "st" (Bool "(" (Bool (Set (Var "q")) "is" ($#v5_orders_3 :::"monotone"::: ) ) & (Bool (Set (Var "i")) "is" ($#v5_orders_3 :::"monotone"::: ) ) & (Bool (Set (Var "f")) ($#r2_funct_2 :::"="::: ) (Set (Set (Var "i")) ($#k1_partfun1 :::"*"::: ) (Set (Var "q")))) & (Bool (Set ($#k3_struct_0 :::"id"::: ) (Set (Var "T"))) ($#r2_funct_2 :::"="::: ) (Set (Set (Var "q")) ($#k1_partfun1 :::"*"::: ) (Set (Var "i")))) ")" ))))) "holds" (Bool (Set (Var "f")) "is" ($#v6_waybel_1 :::"projection"::: ) ))) ; theorem :: WAYBEL_1:36 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "L")) "," (Set (Var "L")) "st" (Bool (Bool (Set (Var "f")) "is" ($#v7_waybel_1 :::"closure"::: ) )) "holds" (Bool (Set ($#k1_waybel_1 :::"["::: ) (Set "(" ($#k3_waybel_1 :::"inclusion"::: ) (Set (Var "f")) ")" ) "," (Set "(" ($#k2_waybel_1 :::"corestr"::: ) (Set (Var "f")) ")" ) ($#k1_waybel_1 :::"]"::: ) ) "is" ($#v3_waybel_1 :::"Galois"::: ) ))) ; theorem :: WAYBEL_1:37 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "L")) "," (Set (Var "L")) "st" (Bool (Bool (Set (Var "f")) "is" ($#v7_waybel_1 :::"closure"::: ) )) "holds" (Bool "ex" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"Poset":::)(Bool "ex" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set (Var "L"))(Bool "ex" (Set (Var "d")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "L")) "," (Set (Var "S")) "st" (Bool "(" (Bool (Set ($#k1_waybel_1 :::"["::: ) (Set (Var "g")) "," (Set (Var "d")) ($#k1_waybel_1 :::"]"::: ) ) "is" ($#v3_waybel_1 :::"Galois"::: ) ) & (Bool (Set (Var "f")) ($#r2_funct_2 :::"="::: ) (Set (Set (Var "g")) ($#k1_partfun1 :::"*"::: ) (Set (Var "d")))) ")" )))))) ; theorem :: WAYBEL_1:38 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "L")) "," (Set (Var "L")) "st" (Bool (Bool (Set (Var "f")) "is" ($#v5_orders_3 :::"monotone"::: ) ) & (Bool "ex" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"Poset":::)(Bool "ex" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set (Var "L"))(Bool "ex" (Set (Var "d")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "L")) "," (Set (Var "S")) "st" (Bool "(" (Bool (Set ($#k1_waybel_1 :::"["::: ) (Set (Var "g")) "," (Set (Var "d")) ($#k1_waybel_1 :::"]"::: ) ) "is" ($#v3_waybel_1 :::"Galois"::: ) ) & (Bool (Set (Var "f")) ($#r2_funct_2 :::"="::: ) (Set (Set (Var "g")) ($#k1_partfun1 :::"*"::: ) (Set (Var "d")))) ")" ))))) "holds" (Bool (Set (Var "f")) "is" ($#v7_waybel_1 :::"closure"::: ) ))) ; theorem :: WAYBEL_1:39 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "L")) "," (Set (Var "L")) "st" (Bool (Bool (Set (Var "f")) "is" ($#v8_waybel_1 :::"kernel"::: ) )) "holds" (Bool (Set ($#k1_waybel_1 :::"["::: ) (Set "(" ($#k2_waybel_1 :::"corestr"::: ) (Set (Var "f")) ")" ) "," (Set "(" ($#k3_waybel_1 :::"inclusion"::: ) (Set (Var "f")) ")" ) ($#k1_waybel_1 :::"]"::: ) ) "is" ($#v3_waybel_1 :::"Galois"::: ) ))) ; theorem :: WAYBEL_1:40 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "L")) "," (Set (Var "L")) "st" (Bool (Bool (Set (Var "f")) "is" ($#v8_waybel_1 :::"kernel"::: ) )) "holds" (Bool "ex" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"Poset":::)(Bool "ex" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "L")) "," (Set (Var "T"))(Bool "ex" (Set (Var "d")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "T")) "," (Set (Var "L")) "st" (Bool "(" (Bool (Set ($#k1_waybel_1 :::"["::: ) (Set (Var "g")) "," (Set (Var "d")) ($#k1_waybel_1 :::"]"::: ) ) "is" ($#v3_waybel_1 :::"Galois"::: ) ) & (Bool (Set (Var "f")) ($#r2_funct_2 :::"="::: ) (Set (Set (Var "d")) ($#k1_partfun1 :::"*"::: ) (Set (Var "g")))) ")" )))))) ; theorem :: WAYBEL_1:41 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "L")) "," (Set (Var "L")) "st" (Bool (Bool (Set (Var "f")) "is" ($#v5_orders_3 :::"monotone"::: ) ) & (Bool "ex" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"Poset":::)(Bool "ex" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "L")) "," (Set (Var "T"))(Bool "ex" (Set (Var "d")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "T")) "," (Set (Var "L")) "st" (Bool "(" (Bool (Set ($#k1_waybel_1 :::"["::: ) (Set (Var "g")) "," (Set (Var "d")) ($#k1_waybel_1 :::"]"::: ) ) "is" ($#v3_waybel_1 :::"Galois"::: ) ) & (Bool (Set (Var "f")) ($#r2_funct_2 :::"="::: ) (Set (Set (Var "d")) ($#k1_partfun1 :::"*"::: ) (Set (Var "g")))) ")" ))))) "holds" (Bool (Set (Var "f")) "is" ($#v8_waybel_1 :::"kernel"::: ) ))) ; theorem :: WAYBEL_1:42 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "L")) "," (Set (Var "L")) "st" (Bool (Bool (Set (Var "p")) "is" ($#v6_waybel_1 :::"projection"::: ) )) "holds" (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set "{" (Set (Var "c")) where c "is" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) : (Bool (Set (Var "c")) ($#r3_orders_2 :::"<="::: ) (Set (Set (Var "p")) ($#k3_funct_2 :::"."::: ) (Set (Var "c")))) "}" ($#k3_xboole_0 :::"/\"::: ) "{" (Set (Var "k")) where k "is" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) : (Bool (Set (Set (Var "p")) ($#k3_funct_2 :::"."::: ) (Set (Var "k"))) ($#r3_orders_2 :::"<="::: ) (Set (Var "k"))) "}" )))) ; theorem :: WAYBEL_1:43 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "L")) "," (Set (Var "L")) "st" (Bool (Bool (Set (Var "p")) "is" ($#v6_waybel_1 :::"projection"::: ) )) "holds" (Bool "(" (Bool "{" (Set (Var "c")) where c "is" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) : (Bool (Set (Var "c")) ($#r3_orders_2 :::"<="::: ) (Set (Set (Var "p")) ($#k3_funct_2 :::"."::: ) (Set (Var "c")))) "}" "is" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L"))) & (Bool "{" (Set (Var "k")) where k "is" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) : (Bool (Set (Set (Var "p")) ($#k3_funct_2 :::"."::: ) (Set (Var "k"))) ($#r3_orders_2 :::"<="::: ) (Set (Var "k"))) "}" "is" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L"))) ")" ))) ; theorem :: WAYBEL_1:44 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "L")) "," (Set (Var "L")) "st" (Bool (Bool (Set (Var "p")) "is" ($#v6_waybel_1 :::"projection"::: ) )) "holds" (Bool "(" (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set "(" (Set (Var "p")) ($#k2_partfun1 :::"|"::: ) "{" (Set (Var "c")) where c "is" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) : (Bool (Set (Var "c")) ($#r3_orders_2 :::"<="::: ) (Set (Set (Var "p")) ($#k3_funct_2 :::"."::: ) (Set (Var "c")))) "}" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "p")))) & (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set "(" (Set (Var "p")) ($#k2_partfun1 :::"|"::: ) "{" (Set (Var "k")) where k "is" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) : (Bool (Set (Set (Var "p")) ($#k3_funct_2 :::"."::: ) (Set (Var "k"))) ($#r3_orders_2 :::"<="::: ) (Set (Var "k"))) "}" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "p")))) ")" ))) ; theorem :: WAYBEL_1:45 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "L")) "," (Set (Var "L")) "st" (Bool (Bool (Set (Var "p")) "is" ($#v6_waybel_1 :::"projection"::: ) )) "holds" (Bool "for" (Set (Var "Lc")) "," (Set (Var "Lk")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "Lc")) ($#r1_hidden :::"="::: ) "{" (Set (Var "c")) where c "is" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) : (Bool (Set (Var "c")) ($#r3_orders_2 :::"<="::: ) (Set (Set (Var "p")) ($#k3_funct_2 :::"."::: ) (Set (Var "c")))) "}" )) "holds" (Bool (Set (Set (Var "p")) ($#k2_partfun1 :::"|"::: ) (Set (Var "Lc"))) "is" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k5_yellow_0 :::"subrelstr"::: ) (Set (Var "Lc")) ")" ) "," (Set "(" ($#k5_yellow_0 :::"subrelstr"::: ) (Set (Var "Lc")) ")" ))))) ; theorem :: WAYBEL_1:46 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "L")) "," (Set (Var "L")) "st" (Bool (Bool (Set (Var "p")) "is" ($#v6_waybel_1 :::"projection"::: ) )) "holds" (Bool "for" (Set (Var "Lk")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "Lk")) ($#r1_hidden :::"="::: ) "{" (Set (Var "k")) where k "is" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) : (Bool (Set (Set (Var "p")) ($#k3_funct_2 :::"."::: ) (Set (Var "k"))) ($#r3_orders_2 :::"<="::: ) (Set (Var "k"))) "}" )) "holds" (Bool (Set (Set (Var "p")) ($#k2_partfun1 :::"|"::: ) (Set (Var "Lk"))) "is" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k5_yellow_0 :::"subrelstr"::: ) (Set (Var "Lk")) ")" ) "," (Set "(" ($#k5_yellow_0 :::"subrelstr"::: ) (Set (Var "Lk")) ")" ))))) ; theorem :: WAYBEL_1:47 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "L")) "," (Set (Var "L")) "st" (Bool (Bool (Set (Var "p")) "is" ($#v6_waybel_1 :::"projection"::: ) )) "holds" (Bool "for" (Set (Var "Lc")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "Lc")) ($#r1_hidden :::"="::: ) "{" (Set (Var "c")) where c "is" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) : (Bool (Set (Var "c")) ($#r3_orders_2 :::"<="::: ) (Set (Set (Var "p")) ($#k3_funct_2 :::"."::: ) (Set (Var "c")))) "}" )) "holds" (Bool "for" (Set (Var "pc")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k5_yellow_0 :::"subrelstr"::: ) (Set (Var "Lc")) ")" ) "," (Set "(" ($#k5_yellow_0 :::"subrelstr"::: ) (Set (Var "Lc")) ")" ) "st" (Bool (Bool (Set (Var "pc")) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k2_partfun1 :::"|"::: ) (Set (Var "Lc"))))) "holds" (Bool (Set (Var "pc")) "is" ($#v7_waybel_1 :::"closure"::: ) ))))) ; theorem :: WAYBEL_1:48 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "L")) "," (Set (Var "L")) "st" (Bool (Bool (Set (Var "p")) "is" ($#v6_waybel_1 :::"projection"::: ) )) "holds" (Bool "for" (Set (Var "Lk")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "Lk")) ($#r1_hidden :::"="::: ) "{" (Set (Var "k")) where k "is" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) : (Bool (Set (Set (Var "p")) ($#k3_funct_2 :::"."::: ) (Set (Var "k"))) ($#r3_orders_2 :::"<="::: ) (Set (Var "k"))) "}" )) "holds" (Bool "for" (Set (Var "pk")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k5_yellow_0 :::"subrelstr"::: ) (Set (Var "Lk")) ")" ) "," (Set "(" ($#k5_yellow_0 :::"subrelstr"::: ) (Set (Var "Lk")) ")" ) "st" (Bool (Bool (Set (Var "pk")) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k2_partfun1 :::"|"::: ) (Set (Var "Lk"))))) "holds" (Bool (Set (Var "pk")) "is" ($#v8_waybel_1 :::"kernel"::: ) ))))) ; theorem :: WAYBEL_1:49 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "L")) "," (Set (Var "L")) "st" (Bool (Bool (Set (Var "p")) "is" ($#v5_orders_3 :::"monotone"::: ) )) "holds" (Bool "for" (Set (Var "Lc")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "Lc")) ($#r1_hidden :::"="::: ) "{" (Set (Var "c")) where c "is" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) : (Bool (Set (Var "c")) ($#r3_orders_2 :::"<="::: ) (Set (Set (Var "p")) ($#k3_funct_2 :::"."::: ) (Set (Var "c")))) "}" )) "holds" (Bool (Set ($#k5_yellow_0 :::"subrelstr"::: ) (Set (Var "Lc"))) "is" ($#v8_yellow_0 :::"sups-inheriting"::: ) )))) ; theorem :: WAYBEL_1:50 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "L")) "," (Set (Var "L")) "st" (Bool (Bool (Set (Var "p")) "is" ($#v5_orders_3 :::"monotone"::: ) )) "holds" (Bool "for" (Set (Var "Lk")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "Lk")) ($#r1_hidden :::"="::: ) "{" (Set (Var "k")) where k "is" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) : (Bool (Set (Set (Var "p")) ($#k3_funct_2 :::"."::: ) (Set (Var "k"))) ($#r3_orders_2 :::"<="::: ) (Set (Var "k"))) "}" )) "holds" (Bool (Set ($#k5_yellow_0 :::"subrelstr"::: ) (Set (Var "Lk"))) "is" ($#v7_yellow_0 :::"infs-inheriting"::: ) )))) ; theorem :: WAYBEL_1:51 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "L")) "," (Set (Var "L")) "st" (Bool (Bool (Set (Var "p")) "is" ($#v6_waybel_1 :::"projection"::: ) )) "holds" (Bool "for" (Set (Var "Lc")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "Lc")) ($#r1_hidden :::"="::: ) "{" (Set (Var "c")) where c "is" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) : (Bool (Set (Var "c")) ($#r3_orders_2 :::"<="::: ) (Set (Set (Var "p")) ($#k3_funct_2 :::"."::: ) (Set (Var "c")))) "}" )) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "p")) "is" ($#v17_waybel_0 :::"infs-preserving"::: ) )) "implies" (Bool "(" (Bool (Set ($#k5_yellow_0 :::"subrelstr"::: ) (Set (Var "Lc"))) "is" ($#v7_yellow_0 :::"infs-inheriting"::: ) ) & (Bool (Set ($#k1_yellow_2 :::"Image"::: ) (Set (Var "p"))) "is" ($#v7_yellow_0 :::"infs-inheriting"::: ) ) ")" ) ")" & "(" (Bool (Bool (Set (Var "p")) "is" ($#v21_waybel_0 :::"filtered-infs-preserving"::: ) )) "implies" (Bool "(" (Bool (Set ($#k5_yellow_0 :::"subrelstr"::: ) (Set (Var "Lc"))) "is" ($#v3_waybel_0 :::"filtered-infs-inheriting"::: ) ) & (Bool (Set ($#k1_yellow_2 :::"Image"::: ) (Set (Var "p"))) "is" ($#v3_waybel_0 :::"filtered-infs-inheriting"::: ) ) ")" ) ")" ")" )))) ; theorem :: WAYBEL_1:52 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "L")) "," (Set (Var "L")) "st" (Bool (Bool (Set (Var "p")) "is" ($#v6_waybel_1 :::"projection"::: ) )) "holds" (Bool "for" (Set (Var "Lk")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "Lk")) ($#r1_hidden :::"="::: ) "{" (Set (Var "k")) where k "is" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) : (Bool (Set (Set (Var "p")) ($#k3_funct_2 :::"."::: ) (Set (Var "k"))) ($#r3_orders_2 :::"<="::: ) (Set (Var "k"))) "}" )) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "p")) "is" ($#v18_waybel_0 :::"sups-preserving"::: ) )) "implies" (Bool "(" (Bool (Set ($#k5_yellow_0 :::"subrelstr"::: ) (Set (Var "Lk"))) "is" ($#v8_yellow_0 :::"sups-inheriting"::: ) ) & (Bool (Set ($#k1_yellow_2 :::"Image"::: ) (Set (Var "p"))) "is" ($#v8_yellow_0 :::"sups-inheriting"::: ) ) ")" ) ")" & "(" (Bool (Bool (Set (Var "p")) "is" ($#v22_waybel_0 :::"directed-sups-preserving"::: ) )) "implies" (Bool "(" (Bool (Set ($#k5_yellow_0 :::"subrelstr"::: ) (Set (Var "Lk"))) "is" ($#v4_waybel_0 :::"directed-sups-inheriting"::: ) ) & (Bool (Set ($#k1_yellow_2 :::"Image"::: ) (Set (Var "p"))) "is" ($#v4_waybel_0 :::"directed-sups-inheriting"::: ) ) ")" ) ")" ")" )))) ; theorem :: WAYBEL_1:53 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "L")) "," (Set (Var "L")) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "p")) "is" ($#v7_waybel_1 :::"closure"::: ) )) "implies" (Bool (Set ($#k1_yellow_2 :::"Image"::: ) (Set (Var "p"))) "is" ($#v7_yellow_0 :::"infs-inheriting"::: ) ) ")" & "(" (Bool (Bool (Set (Var "p")) "is" ($#v8_waybel_1 :::"kernel"::: ) )) "implies" (Bool (Set ($#k1_yellow_2 :::"Image"::: ) (Set (Var "p"))) "is" ($#v8_yellow_0 :::"sups-inheriting"::: ) ) ")" ")" ))) ; theorem :: WAYBEL_1:54 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_lattice3 :::"complete"::: ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "L")) "," (Set (Var "L")) "st" (Bool (Bool (Set (Var "p")) "is" ($#v6_waybel_1 :::"projection"::: ) )) "holds" (Bool (Set ($#k1_yellow_2 :::"Image"::: ) (Set (Var "p"))) "is" ($#v3_lattice3 :::"complete"::: ) ))) ; theorem :: WAYBEL_1:55 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "L")) "," (Set (Var "L")) "st" (Bool (Bool (Set (Var "c")) "is" ($#v7_waybel_1 :::"closure"::: ) )) "holds" (Bool "(" (Bool (Set ($#k2_waybel_1 :::"corestr"::: ) (Set (Var "c"))) "is" ($#v18_waybel_0 :::"sups-preserving"::: ) ) & (Bool "(" "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k1_yellow_2 :::"Image"::: ) (Set (Var "c")) ")" ))) & (Bool ($#r1_yellow_0 :::"ex_sup_of"::: ) (Set (Var "X")) "," (Set (Var "L")))) "holds" (Bool "(" (Bool ($#r1_yellow_0 :::"ex_sup_of"::: ) (Set (Var "X")) "," (Set ($#k1_yellow_2 :::"Image"::: ) (Set (Var "c")))) & (Bool (Set ($#k1_yellow_0 :::""\/""::: ) "(" (Set (Var "X")) "," (Set "(" ($#k1_yellow_2 :::"Image"::: ) (Set (Var "c")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "c")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k1_yellow_0 :::""\/""::: ) "(" (Set (Var "X")) "," (Set (Var "L")) ")" ")" ))) ")" ) ")" ) ")" ))) ; theorem :: WAYBEL_1:56 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "k")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "L")) "," (Set (Var "L")) "st" (Bool (Bool (Set (Var "k")) "is" ($#v8_waybel_1 :::"kernel"::: ) )) "holds" (Bool "(" (Bool (Set ($#k2_waybel_1 :::"corestr"::: ) (Set (Var "k"))) "is" ($#v17_waybel_0 :::"infs-preserving"::: ) ) & (Bool "(" "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k1_yellow_2 :::"Image"::: ) (Set (Var "k")) ")" ))) & (Bool ($#r2_yellow_0 :::"ex_inf_of"::: ) (Set (Var "X")) "," (Set (Var "L")))) "holds" (Bool "(" (Bool ($#r2_yellow_0 :::"ex_inf_of"::: ) (Set (Var "X")) "," (Set ($#k1_yellow_2 :::"Image"::: ) (Set (Var "k")))) & (Bool (Set ($#k2_yellow_0 :::""/\""::: ) "(" (Set (Var "X")) "," (Set "(" ($#k1_yellow_2 :::"Image"::: ) (Set (Var "k")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "k")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k2_yellow_0 :::""/\""::: ) "(" (Set (Var "X")) "," (Set (Var "L")) ")" ")" ))) ")" ) ")" ) ")" ))) ; begin theorem :: WAYBEL_1:57 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_lattice3 :::"complete"::: ) ($#l1_orders_2 :::"Poset":::) "holds" (Bool "(" (Bool (Set ($#k1_waybel_1 :::"["::: ) (Set "(" ($#k3_yellow_2 :::"IdsMap"::: ) (Set (Var "L")) ")" ) "," (Set "(" ($#k2_yellow_2 :::"SupMap"::: ) (Set (Var "L")) ")" ) ($#k1_waybel_1 :::"]"::: ) ) "is" ($#v3_waybel_1 :::"Galois"::: ) ) & (Bool (Set ($#k2_yellow_2 :::"SupMap"::: ) (Set (Var "L"))) "is" ($#v18_waybel_0 :::"sups-preserving"::: ) ) ")" )) ; theorem :: WAYBEL_1:58 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_lattice3 :::"complete"::: ) ($#l1_orders_2 :::"Poset":::) "holds" (Bool "(" (Bool (Set (Set "(" ($#k3_yellow_2 :::"IdsMap"::: ) (Set (Var "L")) ")" ) ($#k1_partfun1 :::"*"::: ) (Set "(" ($#k2_yellow_2 :::"SupMap"::: ) (Set (Var "L")) ")" )) "is" ($#v7_waybel_1 :::"closure"::: ) ) & (Bool (Set ($#k1_yellow_2 :::"Image"::: ) (Set "(" (Set "(" ($#k3_yellow_2 :::"IdsMap"::: ) (Set (Var "L")) ")" ) ($#k1_partfun1 :::"*"::: ) (Set "(" ($#k2_yellow_2 :::"SupMap"::: ) (Set (Var "L")) ")" ) ")" )) "," (Set (Var "L")) ($#r5_waybel_1 :::"are_isomorphic"::: ) ) ")" )) ; definitionlet "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) ; let "x" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "S")); func "x" :::""/\""::: -> ($#m1_subset_1 :::"Function":::) "of" "S" "," "S" means :: WAYBEL_1:def 18 (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"Element":::) "of" "S" "holds" (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) (Set "x" ($#k11_lattice3 :::""/\""::: ) (Set (Var "s"))))); end; :: deftheorem defines :::""/\""::: WAYBEL_1:def 18 : (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set (Var "S")) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k4_waybel_1 :::""/\""::: ) )) "iff" (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) "holds" (Bool (Set (Set (Var "b3")) ($#k3_funct_2 :::"."::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k11_lattice3 :::""/\""::: ) (Set (Var "s"))))) ")" )))); theorem :: WAYBEL_1:59 (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "t")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) "holds" (Bool "{" (Set (Var "s")) where s "is" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) : (Bool (Set (Set (Var "x")) ($#k11_lattice3 :::""/\""::: ) (Set (Var "s"))) ($#r1_orders_2 :::"<="::: ) (Set (Var "t"))) "}" ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "x")) ($#k4_waybel_1 :::""/\""::: ) ")" ) ($#k8_relset_1 :::"""::: ) (Set "(" ($#k5_waybel_0 :::"downarrow"::: ) (Set (Var "t")) ")" ))))) ; theorem :: WAYBEL_1:60 (Bool "for" (Set (Var "S")) "being" ($#l1_orders_2 :::"Semilattice":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) "holds" (Bool (Set (Set (Var "x")) ($#k4_waybel_1 :::""/\""::: ) ) "is" ($#v5_orders_3 :::"monotone"::: ) ))) ; registrationlet "S" be ($#l1_orders_2 :::"Semilattice":::); let "x" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "S")); cluster (Set "x" ($#k4_waybel_1 :::""/\""::: ) ) -> ($#v5_orders_3 :::"monotone"::: ) ; end; theorem :: WAYBEL_1:61 (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "S")) "holds" (Bool (Set (Set "(" (Set (Var "x")) ($#k4_waybel_1 :::""/\""::: ) ")" ) ($#k7_relset_1 :::".:"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) "{" (Set "(" (Set (Var "x")) ($#k11_lattice3 :::""/\""::: ) (Set (Var "y")) ")" ) where y "is" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) : (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) "}" )))) ; theorem :: WAYBEL_1:62 (Bool "for" (Set (Var "S")) "being" ($#l1_orders_2 :::"Semilattice":::) "holds" (Bool "(" (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) "holds" (Bool (Set (Set (Var "x")) ($#k4_waybel_1 :::""/\""::: ) ) "is" ($#v5_waybel_1 :::"lower_adjoint"::: ) ) ")" ) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "t")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) "holds" (Bool ($#r2_waybel_1 :::"ex_max_of"::: ) "{" (Set (Var "s")) where s "is" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) : (Bool (Set (Set (Var "x")) ($#k12_lattice3 :::""/\""::: ) (Set (Var "s"))) ($#r3_orders_2 :::"<="::: ) (Set (Var "t"))) "}" "," (Set (Var "S")))) ")" )) ; theorem :: WAYBEL_1:63 (Bool "for" (Set (Var "S")) "being" ($#l1_orders_2 :::"Semilattice":::) "st" (Bool (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) "holds" (Bool (Set (Set (Var "x")) ($#k4_waybel_1 :::""/\""::: ) ) "is" ($#v5_waybel_1 :::"lower_adjoint"::: ) ) ")" )) "holds" (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "S")) "st" (Bool (Bool ($#r1_yellow_0 :::"ex_sup_of"::: ) (Set (Var "X")) "," (Set (Var "S")))) "holds" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) "holds" (Bool (Set (Set (Var "x")) ($#k12_lattice3 :::""/\""::: ) (Set "(" ($#k1_yellow_0 :::""\/""::: ) "(" (Set (Var "X")) "," (Set (Var "S")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_yellow_0 :::""\/""::: ) "(" "{" (Set "(" (Set (Var "x")) ($#k12_lattice3 :::""/\""::: ) (Set (Var "y")) ")" ) where y "is" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) : (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) "}" "," (Set (Var "S")) ")" ))))) ; theorem :: WAYBEL_1:64 (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_lattice3 :::"complete"::: ) ($#l1_orders_2 :::"Poset":::) "holds" (Bool "(" (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) "holds" (Bool (Set (Set (Var "x")) ($#k4_waybel_1 :::""/\""::: ) ) "is" ($#v5_waybel_1 :::"lower_adjoint"::: ) ) ")" ) "iff" (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) "holds" (Bool (Set (Set (Var "x")) ($#k12_lattice3 :::""/\""::: ) (Set "(" ($#k1_yellow_0 :::""\/""::: ) "(" (Set (Var "X")) "," (Set (Var "S")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_yellow_0 :::""\/""::: ) "(" "{" (Set "(" (Set (Var "x")) ($#k12_lattice3 :::""/\""::: ) (Set (Var "y")) ")" ) where y "is" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) : (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) "}" "," (Set (Var "S")) ")" )))) ")" )) ; theorem :: WAYBEL_1:65 (Bool "for" (Set (Var "S")) "being" ($#l1_orders_2 :::"LATTICE":::) "st" (Bool (Bool "(" "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "S")) "st" (Bool (Bool ($#r1_yellow_0 :::"ex_sup_of"::: ) (Set (Var "X")) "," (Set (Var "S")))) "holds" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) "holds" (Bool (Set (Set (Var "x")) ($#k12_lattice3 :::""/\""::: ) (Set "(" ($#k1_yellow_0 :::""\/""::: ) "(" (Set (Var "X")) "," (Set (Var "S")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_yellow_0 :::""\/""::: ) "(" "{" (Set "(" (Set (Var "x")) ($#k12_lattice3 :::""/\""::: ) (Set (Var "y")) ")" ) where y "is" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) : (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) "}" "," (Set (Var "S")) ")" ))) ")" )) "holds" (Bool (Set (Var "S")) "is" ($#v2_waybel_1 :::"distributive"::: ) )) ; definitionlet "H" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) ; attr "H" is :::"Heyting"::: means :: WAYBEL_1:def 19 (Bool "(" (Bool "H" "is" ($#l1_orders_2 :::"LATTICE":::)) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" "H" "holds" (Bool (Set (Set (Var "x")) ($#k4_waybel_1 :::""/\""::: ) ) "is" ($#v5_waybel_1 :::"lower_adjoint"::: ) ) ")" ) ")" ); end; :: deftheorem defines :::"Heyting"::: WAYBEL_1:def 19 : (Bool "for" (Set (Var "H")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) "holds" (Bool "(" (Bool (Set (Var "H")) "is" ($#v9_waybel_1 :::"Heyting"::: ) ) "iff" (Bool "(" (Bool (Set (Var "H")) "is" ($#l1_orders_2 :::"LATTICE":::)) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "H")) "holds" (Bool (Set (Set (Var "x")) ($#k4_waybel_1 :::""/\""::: ) ) "is" ($#v5_waybel_1 :::"lower_adjoint"::: ) ) ")" ) ")" ) ")" )); registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v9_waybel_1 :::"Heyting"::: ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#v4_orders_2 :::"transitive"::: ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#v1_lattice3 :::"with_suprema"::: ) ($#v2_lattice3 :::"with_infima"::: ) for ($#l1_orders_2 :::"RelStr"::: ) ; end; definitionlet "H" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) ; let "a" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "H")); assume (Bool (Set (Const "H")) "is" ($#v9_waybel_1 :::"Heyting"::: ) ) ; func "a" :::"=>"::: -> ($#m1_subset_1 :::"Function":::) "of" "H" "," "H" means :: WAYBEL_1:def 20 (Bool (Set ($#k1_waybel_1 :::"["::: ) it "," (Set "(" "a" ($#k4_waybel_1 :::""/\""::: ) ")" ) ($#k1_waybel_1 :::"]"::: ) ) "is" ($#v3_waybel_1 :::"Galois"::: ) ); end; :: deftheorem defines :::"=>"::: WAYBEL_1:def 20 : (Bool "for" (Set (Var "H")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "H")) "st" (Bool (Bool (Set (Var "H")) "is" ($#v9_waybel_1 :::"Heyting"::: ) )) "holds" (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "H")) "," (Set (Var "H")) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k5_waybel_1 :::"=>"::: ) )) "iff" (Bool (Set ($#k1_waybel_1 :::"["::: ) (Set (Var "b3")) "," (Set "(" (Set (Var "a")) ($#k4_waybel_1 :::""/\""::: ) ")" ) ($#k1_waybel_1 :::"]"::: ) ) "is" ($#v3_waybel_1 :::"Galois"::: ) ) ")" )))); theorem :: WAYBEL_1:66 (Bool "for" (Set (Var "H")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) "st" (Bool (Bool (Set (Var "H")) "is" ($#v9_waybel_1 :::"Heyting"::: ) )) "holds" (Bool (Set (Var "H")) "is" ($#v2_waybel_1 :::"distributive"::: ) )) ; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v9_waybel_1 :::"Heyting"::: ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_waybel_1 :::"distributive"::: ) for ($#l1_orders_2 :::"RelStr"::: ) ; end; definitionlet "H" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) ; let "a", "y" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "H")); func "a" :::"=>"::: "y" -> ($#m1_subset_1 :::"Element":::) "of" "H" equals :: WAYBEL_1:def 21 (Set (Set "(" "a" ($#k5_waybel_1 :::"=>"::: ) ")" ) ($#k3_funct_2 :::"."::: ) "y"); end; :: deftheorem defines :::"=>"::: WAYBEL_1:def 21 : (Bool "for" (Set (Var "H")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "a")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "H")) "holds" (Bool (Set (Set (Var "a")) ($#k6_waybel_1 :::"=>"::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k5_waybel_1 :::"=>"::: ) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "y")))))); theorem :: WAYBEL_1:67 (Bool "for" (Set (Var "H")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) "st" (Bool (Bool (Set (Var "H")) "is" ($#v9_waybel_1 :::"Heyting"::: ) )) "holds" (Bool "for" (Set (Var "x")) "," (Set (Var "a")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "H")) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r1_orders_2 :::">="::: ) (Set (Set (Var "a")) ($#k11_lattice3 :::""/\""::: ) (Set (Var "y")))) "iff" (Bool (Set (Set (Var "a")) ($#k6_waybel_1 :::"=>"::: ) (Set (Var "x"))) ($#r1_orders_2 :::">="::: ) (Set (Var "y"))) ")" ))) ; theorem :: WAYBEL_1:68 (Bool "for" (Set (Var "H")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) "st" (Bool (Bool (Set (Var "H")) "is" ($#v9_waybel_1 :::"Heyting"::: ) )) "holds" (Bool (Set (Var "H")) "is" ($#v2_yellow_0 :::"upper-bounded"::: ) )) ; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v9_waybel_1 :::"Heyting"::: ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_yellow_0 :::"upper-bounded"::: ) for ($#l1_orders_2 :::"RelStr"::: ) ; end; theorem :: WAYBEL_1:69 (Bool "for" (Set (Var "H")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) "st" (Bool (Bool (Set (Var "H")) "is" ($#v9_waybel_1 :::"Heyting"::: ) )) "holds" (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "H")) "holds" (Bool "(" (Bool (Set ($#k4_yellow_0 :::"Top"::: ) (Set (Var "H"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k6_waybel_1 :::"=>"::: ) (Set (Var "b")))) "iff" (Bool (Set (Var "a")) ($#r1_orders_2 :::"<="::: ) (Set (Var "b"))) ")" ))) ; theorem :: WAYBEL_1:70 (Bool "for" (Set (Var "H")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) "st" (Bool (Bool (Set (Var "H")) "is" ($#v9_waybel_1 :::"Heyting"::: ) )) "holds" (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "H")) "holds" (Bool (Set ($#k4_yellow_0 :::"Top"::: ) (Set (Var "H"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k6_waybel_1 :::"=>"::: ) (Set (Var "a")))))) ; theorem :: WAYBEL_1:71 (Bool "for" (Set (Var "H")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) "st" (Bool (Bool (Set (Var "H")) "is" ($#v9_waybel_1 :::"Heyting"::: ) )) "holds" (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "H")) "st" (Bool (Bool (Set ($#k4_yellow_0 :::"Top"::: ) (Set (Var "H"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k6_waybel_1 :::"=>"::: ) (Set (Var "b")))) & (Bool (Set ($#k4_yellow_0 :::"Top"::: ) (Set (Var "H"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "b")) ($#k6_waybel_1 :::"=>"::: ) (Set (Var "a"))))) "holds" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Var "b"))))) ; theorem :: WAYBEL_1:72 (Bool "for" (Set (Var "H")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) "st" (Bool (Bool (Set (Var "H")) "is" ($#v9_waybel_1 :::"Heyting"::: ) )) "holds" (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "H")) "holds" (Bool (Set (Var "b")) ($#r1_orders_2 :::"<="::: ) (Set (Set (Var "a")) ($#k6_waybel_1 :::"=>"::: ) (Set (Var "b")))))) ; theorem :: WAYBEL_1:73 (Bool "for" (Set (Var "H")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) "st" (Bool (Bool (Set (Var "H")) "is" ($#v9_waybel_1 :::"Heyting"::: ) )) "holds" (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "H")) "holds" (Bool (Set ($#k4_yellow_0 :::"Top"::: ) (Set (Var "H"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k6_waybel_1 :::"=>"::: ) (Set "(" ($#k4_yellow_0 :::"Top"::: ) (Set (Var "H")) ")" ))))) ; theorem :: WAYBEL_1:74 (Bool "for" (Set (Var "H")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) "st" (Bool (Bool (Set (Var "H")) "is" ($#v9_waybel_1 :::"Heyting"::: ) )) "holds" (Bool "for" (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "H")) "holds" (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_yellow_0 :::"Top"::: ) (Set (Var "H")) ")" ) ($#k6_waybel_1 :::"=>"::: ) (Set (Var "b")))))) ; theorem :: WAYBEL_1:75 (Bool "for" (Set (Var "H")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) "st" (Bool (Bool (Set (Var "H")) "is" ($#v9_waybel_1 :::"Heyting"::: ) )) "holds" (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "H")) "st" (Bool (Bool (Set (Var "a")) ($#r1_orders_2 :::"<="::: ) (Set (Var "b")))) "holds" (Bool (Set (Set (Var "b")) ($#k6_waybel_1 :::"=>"::: ) (Set (Var "c"))) ($#r1_orders_2 :::"<="::: ) (Set (Set (Var "a")) ($#k6_waybel_1 :::"=>"::: ) (Set (Var "c")))))) ; theorem :: WAYBEL_1:76 (Bool "for" (Set (Var "H")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) "st" (Bool (Bool (Set (Var "H")) "is" ($#v9_waybel_1 :::"Heyting"::: ) )) "holds" (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "H")) "st" (Bool (Bool (Set (Var "b")) ($#r1_orders_2 :::"<="::: ) (Set (Var "c")))) "holds" (Bool (Set (Set (Var "a")) ($#k6_waybel_1 :::"=>"::: ) (Set (Var "b"))) ($#r1_orders_2 :::"<="::: ) (Set (Set (Var "a")) ($#k6_waybel_1 :::"=>"::: ) (Set (Var "c")))))) ; theorem :: WAYBEL_1:77 (Bool "for" (Set (Var "H")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) "st" (Bool (Bool (Set (Var "H")) "is" ($#v9_waybel_1 :::"Heyting"::: ) )) "holds" (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "H")) "holds" (Bool (Set (Set (Var "a")) ($#k11_lattice3 :::""/\""::: ) (Set "(" (Set (Var "a")) ($#k6_waybel_1 :::"=>"::: ) (Set (Var "b")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k11_lattice3 :::""/\""::: ) (Set (Var "b")))))) ; theorem :: WAYBEL_1:78 (Bool "for" (Set (Var "H")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) "st" (Bool (Bool (Set (Var "H")) "is" ($#v9_waybel_1 :::"Heyting"::: ) )) "holds" (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "H")) "holds" (Bool (Set (Set "(" (Set (Var "a")) ($#k10_lattice3 :::""\/""::: ) (Set (Var "b")) ")" ) ($#k6_waybel_1 :::"=>"::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k6_waybel_1 :::"=>"::: ) (Set (Var "c")) ")" ) ($#k11_lattice3 :::""/\""::: ) (Set "(" (Set (Var "b")) ($#k6_waybel_1 :::"=>"::: ) (Set (Var "c")) ")" ))))) ; definitionlet "H" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) ; let "a" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "H")); func :::"'not'"::: "a" -> ($#m1_subset_1 :::"Element":::) "of" "H" equals :: WAYBEL_1:def 22 (Set "a" ($#k6_waybel_1 :::"=>"::: ) (Set "(" ($#k3_yellow_0 :::"Bottom"::: ) "H" ")" )); end; :: deftheorem defines :::"'not'"::: WAYBEL_1:def 22 : (Bool "for" (Set (Var "H")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "H")) "holds" (Bool (Set ($#k7_waybel_1 :::"'not'"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k6_waybel_1 :::"=>"::: ) (Set "(" ($#k3_yellow_0 :::"Bottom"::: ) (Set (Var "H")) ")" ))))); theorem :: WAYBEL_1:79 (Bool "for" (Set (Var "H")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) "st" (Bool (Bool (Set (Var "H")) "is" ($#v9_waybel_1 :::"Heyting"::: ) ) & (Bool (Set (Var "H")) "is" ($#v1_yellow_0 :::"lower-bounded"::: ) )) "holds" (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "H")) "holds" (Bool (Set ($#k7_waybel_1 :::"'not'"::: ) (Set (Var "a"))) ($#r4_waybel_1 :::"is_maximum_of"::: ) "{" (Set (Var "x")) where x "is" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "H")) : (Bool (Set (Set (Var "a")) ($#k11_lattice3 :::""/\""::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k3_yellow_0 :::"Bottom"::: ) (Set (Var "H")))) "}" ))) ; theorem :: WAYBEL_1:80 (Bool "for" (Set (Var "H")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) "st" (Bool (Bool (Set (Var "H")) "is" ($#v9_waybel_1 :::"Heyting"::: ) ) & (Bool (Set (Var "H")) "is" ($#v1_yellow_0 :::"lower-bounded"::: ) )) "holds" (Bool "(" (Bool (Set ($#k7_waybel_1 :::"'not'"::: ) (Set "(" ($#k3_yellow_0 :::"Bottom"::: ) (Set (Var "H")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_yellow_0 :::"Top"::: ) (Set (Var "H")))) & (Bool (Set ($#k7_waybel_1 :::"'not'"::: ) (Set "(" ($#k4_yellow_0 :::"Top"::: ) (Set (Var "H")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k3_yellow_0 :::"Bottom"::: ) (Set (Var "H")))) ")" )) ; theorem :: WAYBEL_1:81 (Bool "for" (Set (Var "H")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_yellow_0 :::"lower-bounded"::: ) ($#l1_orders_2 :::"RelStr"::: ) "st" (Bool (Bool (Set (Var "H")) "is" ($#v9_waybel_1 :::"Heyting"::: ) )) "holds" (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "H")) "holds" (Bool "(" (Bool (Set ($#k7_waybel_1 :::"'not'"::: ) (Set (Var "a"))) ($#r1_orders_2 :::">="::: ) (Set (Var "b"))) "iff" (Bool (Set ($#k7_waybel_1 :::"'not'"::: ) (Set (Var "b"))) ($#r1_orders_2 :::">="::: ) (Set (Var "a"))) ")" ))) ; theorem :: WAYBEL_1:82 (Bool "for" (Set (Var "H")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_yellow_0 :::"lower-bounded"::: ) ($#l1_orders_2 :::"RelStr"::: ) "st" (Bool (Bool (Set (Var "H")) "is" ($#v9_waybel_1 :::"Heyting"::: ) )) "holds" (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "H")) "holds" (Bool "(" (Bool (Set ($#k7_waybel_1 :::"'not'"::: ) (Set (Var "a"))) ($#r1_orders_2 :::">="::: ) (Set (Var "b"))) "iff" (Bool (Set (Set (Var "a")) ($#k11_lattice3 :::""/\""::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set ($#k3_yellow_0 :::"Bottom"::: ) (Set (Var "H")))) ")" ))) ; theorem :: WAYBEL_1:83 (Bool "for" (Set (Var "H")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_yellow_0 :::"lower-bounded"::: ) ($#l1_orders_2 :::"RelStr"::: ) "st" (Bool (Bool (Set (Var "H")) "is" ($#v9_waybel_1 :::"Heyting"::: ) )) "holds" (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "H")) "st" (Bool (Bool (Set (Var "a")) ($#r1_orders_2 :::"<="::: ) (Set (Var "b")))) "holds" (Bool (Set ($#k7_waybel_1 :::"'not'"::: ) (Set (Var "b"))) ($#r1_orders_2 :::"<="::: ) (Set ($#k7_waybel_1 :::"'not'"::: ) (Set (Var "a")))))) ; theorem :: WAYBEL_1:84 (Bool "for" (Set (Var "H")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_yellow_0 :::"lower-bounded"::: ) ($#l1_orders_2 :::"RelStr"::: ) "st" (Bool (Bool (Set (Var "H")) "is" ($#v9_waybel_1 :::"Heyting"::: ) )) "holds" (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "H")) "holds" (Bool (Set ($#k7_waybel_1 :::"'not'"::: ) (Set "(" (Set (Var "a")) ($#k10_lattice3 :::""\/""::: ) (Set (Var "b")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k7_waybel_1 :::"'not'"::: ) (Set (Var "a")) ")" ) ($#k11_lattice3 :::""/\""::: ) (Set "(" ($#k7_waybel_1 :::"'not'"::: ) (Set (Var "b")) ")" ))))) ; theorem :: WAYBEL_1:85 (Bool "for" (Set (Var "H")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_yellow_0 :::"lower-bounded"::: ) ($#l1_orders_2 :::"RelStr"::: ) "st" (Bool (Bool (Set (Var "H")) "is" ($#v9_waybel_1 :::"Heyting"::: ) )) "holds" (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "H")) "holds" (Bool (Set ($#k7_waybel_1 :::"'not'"::: ) (Set "(" (Set (Var "a")) ($#k11_lattice3 :::""/\""::: ) (Set (Var "b")) ")" )) ($#r1_orders_2 :::">="::: ) (Set (Set "(" ($#k7_waybel_1 :::"'not'"::: ) (Set (Var "a")) ")" ) ($#k10_lattice3 :::""\/""::: ) (Set "(" ($#k7_waybel_1 :::"'not'"::: ) (Set (Var "b")) ")" ))))) ; definitionlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) ; let "x", "y" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "L")); pred "y" :::"is_a_complement_of"::: "x" means :: WAYBEL_1:def 23 (Bool "(" (Bool (Set "x" ($#k10_lattice3 :::""\/""::: ) "y") ($#r1_hidden :::"="::: ) (Set ($#k4_yellow_0 :::"Top"::: ) "L")) & (Bool (Set "x" ($#k11_lattice3 :::""/\""::: ) "y") ($#r1_hidden :::"="::: ) (Set ($#k3_yellow_0 :::"Bottom"::: ) "L")) ")" ); end; :: deftheorem defines :::"is_a_complement_of"::: WAYBEL_1:def 23 : (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "y")) ($#r6_waybel_1 :::"is_a_complement_of"::: ) (Set (Var "x"))) "iff" (Bool "(" (Bool (Set (Set (Var "x")) ($#k10_lattice3 :::""\/""::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set ($#k4_yellow_0 :::"Top"::: ) (Set (Var "L")))) & (Bool (Set (Set (Var "x")) ($#k11_lattice3 :::""/\""::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set ($#k3_yellow_0 :::"Bottom"::: ) (Set (Var "L")))) ")" ) ")" ))); definitionlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) ; attr "L" is :::"complemented"::: means :: WAYBEL_1:def 24 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" "L" (Bool "ex" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" "L" "st" (Bool (Set (Var "y")) ($#r6_waybel_1 :::"is_a_complement_of"::: ) (Set (Var "x"))))); end; :: deftheorem defines :::"complemented"::: WAYBEL_1:def 24 : (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) "holds" (Bool "(" (Bool (Set (Var "L")) "is" ($#v10_waybel_1 :::"complemented"::: ) ) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) (Bool "ex" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Set (Var "y")) ($#r6_waybel_1 :::"is_a_complement_of"::: ) (Set (Var "x"))))) ")" )); registrationlet "X" be ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k3_yellow_1 :::"BoolePoset"::: ) "X") -> ($#v10_waybel_1 :::"complemented"::: ) ; end; theorem :: WAYBEL_1:86 (Bool "for" (Set (Var "L")) "being" ($#v3_yellow_0 :::"bounded"::: ) ($#l1_orders_2 :::"LATTICE":::) "st" (Bool (Bool (Set (Var "L")) "is" ($#v9_waybel_1 :::"Heyting"::: ) ) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set ($#k7_waybel_1 :::"'not'"::: ) (Set "(" ($#k7_waybel_1 :::"'not'"::: ) (Set (Var "x")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "x"))) ")" )) "holds" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set ($#k7_waybel_1 :::"'not'"::: ) (Set (Var "x"))) ($#r6_waybel_1 :::"is_a_complement_of"::: ) (Set (Var "x"))))) ; theorem :: WAYBEL_1:87 (Bool "for" (Set (Var "L")) "being" ($#v3_yellow_0 :::"bounded"::: ) ($#l1_orders_2 :::"LATTICE":::) "holds" (Bool "(" (Bool (Set (Var "L")) "is" ($#v2_waybel_1 :::"distributive"::: ) ) & (Bool (Set (Var "L")) "is" ($#v10_waybel_1 :::"complemented"::: ) ) "iff" (Bool "(" (Bool (Set (Var "L")) "is" ($#v9_waybel_1 :::"Heyting"::: ) ) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set ($#k7_waybel_1 :::"'not'"::: ) (Set "(" ($#k7_waybel_1 :::"'not'"::: ) (Set (Var "x")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "x"))) ")" ) ")" ) ")" )) ; definitionlet "B" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) ; attr "B" is :::"Boolean"::: means :: WAYBEL_1:def 25 (Bool "(" (Bool "B" "is" ($#l1_orders_2 :::"LATTICE":::)) & (Bool "B" "is" ($#v3_yellow_0 :::"bounded"::: ) ) & (Bool "B" "is" ($#v2_waybel_1 :::"distributive"::: ) ) & (Bool "B" "is" ($#v10_waybel_1 :::"complemented"::: ) ) ")" ); end; :: deftheorem defines :::"Boolean"::: WAYBEL_1:def 25 : (Bool "for" (Set (Var "B")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) "holds" (Bool "(" (Bool (Set (Var "B")) "is" ($#v11_waybel_1 :::"Boolean"::: ) ) "iff" (Bool "(" (Bool (Set (Var "B")) "is" ($#l1_orders_2 :::"LATTICE":::)) & (Bool (Set (Var "B")) "is" ($#v3_yellow_0 :::"bounded"::: ) ) & (Bool (Set (Var "B")) "is" ($#v2_waybel_1 :::"distributive"::: ) ) & (Bool (Set (Var "B")) "is" ($#v10_waybel_1 :::"complemented"::: ) ) ")" ) ")" )); registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v11_waybel_1 :::"Boolean"::: ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#v4_orders_2 :::"transitive"::: ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#v1_lattice3 :::"with_suprema"::: ) ($#v2_lattice3 :::"with_infima"::: ) ($#v3_yellow_0 :::"bounded"::: ) ($#v2_waybel_1 :::"distributive"::: ) ($#v10_waybel_1 :::"complemented"::: ) for ($#l1_orders_2 :::"RelStr"::: ) ; end; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#v4_orders_2 :::"transitive"::: ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#v1_lattice3 :::"with_suprema"::: ) ($#v2_lattice3 :::"with_infima"::: ) ($#v3_yellow_0 :::"bounded"::: ) ($#v2_waybel_1 :::"distributive"::: ) ($#v10_waybel_1 :::"complemented"::: ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v11_waybel_1 :::"Boolean"::: ) for ($#l1_orders_2 :::"RelStr"::: ) ; end; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v11_waybel_1 :::"Boolean"::: ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v9_waybel_1 :::"Heyting"::: ) for ($#l1_orders_2 :::"RelStr"::: ) ; end; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_orders_2 :::"strict"::: ) ($#v3_orders_2 :::"reflexive"::: ) ($#v4_orders_2 :::"transitive"::: ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#v1_lattice3 :::"with_suprema"::: ) ($#v2_lattice3 :::"with_infima"::: ) ($#v11_waybel_1 :::"Boolean"::: ) for ($#l1_orders_2 :::"RelStr"::: ) ; end; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_orders_2 :::"strict"::: ) ($#v3_orders_2 :::"reflexive"::: ) ($#v4_orders_2 :::"transitive"::: ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#v1_lattice3 :::"with_suprema"::: ) ($#v2_lattice3 :::"with_infima"::: ) ($#v9_waybel_1 :::"Heyting"::: ) for ($#l1_orders_2 :::"RelStr"::: ) ; end;