:: WAYBEL22 semantic presentation begin theorem :: WAYBEL22:1 (Bool "for" (Set (Var "L")) "being" ($#v2_yellow_0 :::"upper-bounded"::: ) ($#l1_orders_2 :::"Semilattice":::) (Bool "for" (Set (Var "F")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_waybel_0 :::"directed"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k2_yellow_1 :::"InclPoset"::: ) (Set "(" ($#k8_waybel_0 :::"Filt"::: ) (Set (Var "L")) ")" ) ")" ) "holds" (Bool (Set ($#k1_yellow_0 :::"sup"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set ($#k3_tarski :::"union"::: ) (Set (Var "F")))))) ; theorem :: WAYBEL22:2 (Bool "for" (Set (Var "L")) "," (Set (Var "S")) "," (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_lattice3 :::"complete"::: ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "f")) "being" ($#m1_waybel16 :::"CLHomomorphism"::: ) "of" (Set (Var "L")) "," (Set (Var "S")) (Bool "for" (Set (Var "g")) "being" ($#m1_waybel16 :::"CLHomomorphism"::: ) "of" (Set (Var "S")) "," (Set (Var "T")) "holds" (Bool (Set (Set (Var "g")) ($#k1_partfun1 :::"*"::: ) (Set (Var "f"))) "is" ($#m1_waybel16 :::"CLHomomorphism"::: ) "of" (Set (Var "L")) "," (Set (Var "T")))))) ; theorem :: WAYBEL22:3 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) "holds" (Bool (Set ($#k3_struct_0 :::"id"::: ) (Set (Var "L"))) "is" ($#v17_waybel_0 :::"infs-preserving"::: ) )) ; theorem :: WAYBEL22:4 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) "holds" (Bool (Set ($#k3_struct_0 :::"id"::: ) (Set (Var "L"))) "is" ($#v22_waybel_0 :::"directed-sups-preserving"::: ) )) ; theorem :: WAYBEL22:5 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_lattice3 :::"complete"::: ) ($#l1_orders_2 :::"Poset":::) "holds" (Bool (Set ($#k3_struct_0 :::"id"::: ) (Set (Var "L"))) "is" ($#m1_waybel16 :::"CLHomomorphism"::: ) "of" (Set (Var "L")) "," (Set (Var "L")))) ; theorem :: WAYBEL22:6 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_yellow_0 :::"upper-bounded"::: ) ($#v2_lattice3 :::"with_infima"::: ) ($#l1_orders_2 :::"Poset":::) "holds" (Bool (Set ($#k2_yellow_1 :::"InclPoset"::: ) (Set "(" ($#k8_waybel_0 :::"Filt"::: ) (Set (Var "L")) ")" )) "is" ($#m1_yellow_0 :::"CLSubFrame":::) "of" (Set ($#k3_yellow_1 :::"BoolePoset"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L")))))) ; registrationlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_yellow_0 :::"upper-bounded"::: ) ($#v2_lattice3 :::"with_infima"::: ) ($#l1_orders_2 :::"Poset":::); cluster (Set ($#k2_yellow_1 :::"InclPoset"::: ) (Set "(" ($#k8_waybel_0 :::"Filt"::: ) "L" ")" )) -> ($#v3_waybel_3 :::"continuous"::: ) ; end; registrationlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_yellow_0 :::"upper-bounded"::: ) ($#l1_orders_2 :::"Poset":::); cluster -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k2_yellow_1 :::"InclPoset"::: ) (Set "(" ($#k8_waybel_0 :::"Filt"::: ) "L" ")" ) ")" )); end; begin definitionlet "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_lattice3 :::"complete"::: ) ($#v3_waybel_3 :::"continuous"::: ) ($#l1_orders_2 :::"Poset":::); let "A" be ($#m1_hidden :::"set"::: ) ; pred "A" :::"is_FreeGen_set_of"::: "S" means :: WAYBEL22:def 1 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_lattice3 :::"complete"::: ) ($#v3_waybel_3 :::"continuous"::: ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" "A" "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "T"))) (Bool "ex" (Set (Var "h")) "being" ($#m1_waybel16 :::"CLHomomorphism"::: ) "of" "S" "," (Set (Var "T")) "st" (Bool "(" (Bool (Set (Set (Var "h")) ($#k2_partfun1 :::"|"::: ) "A") ($#r1_hidden :::"="::: ) (Set (Var "f"))) & (Bool "(" "for" (Set (Var "h9")) "being" ($#m1_waybel16 :::"CLHomomorphism"::: ) "of" "S" "," (Set (Var "T")) "st" (Bool (Bool (Set (Set (Var "h9")) ($#k2_partfun1 :::"|"::: ) "A") ($#r1_hidden :::"="::: ) (Set (Var "f")))) "holds" (Bool (Set (Var "h9")) ($#r2_funct_2 :::"="::: ) (Set (Var "h"))) ")" ) ")" )))); end; :: deftheorem defines :::"is_FreeGen_set_of"::: WAYBEL22:def 1 : (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_lattice3 :::"complete"::: ) ($#v3_waybel_3 :::"continuous"::: ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "A")) ($#r1_waybel22 :::"is_FreeGen_set_of"::: ) (Set (Var "S"))) "iff" (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_lattice3 :::"complete"::: ) ($#v3_waybel_3 :::"continuous"::: ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "A")) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "T"))) (Bool "ex" (Set (Var "h")) "being" ($#m1_waybel16 :::"CLHomomorphism"::: ) "of" (Set (Var "S")) "," (Set (Var "T")) "st" (Bool "(" (Bool (Set (Set (Var "h")) ($#k2_partfun1 :::"|"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set (Var "f"))) & (Bool "(" "for" (Set (Var "h9")) "being" ($#m1_waybel16 :::"CLHomomorphism"::: ) "of" (Set (Var "S")) "," (Set (Var "T")) "st" (Bool (Bool (Set (Set (Var "h9")) ($#k2_partfun1 :::"|"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set (Var "f")))) "holds" (Bool (Set (Var "h9")) ($#r2_funct_2 :::"="::: ) (Set (Var "h"))) ")" ) ")" )))) ")" ))); theorem :: WAYBEL22:7 (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_lattice3 :::"complete"::: ) ($#v3_waybel_3 :::"continuous"::: ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "A")) ($#r1_waybel22 :::"is_FreeGen_set_of"::: ) (Set (Var "S")))) "holds" (Bool (Set (Var "A")) "is" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "S"))))) ; theorem :: WAYBEL22:8 (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_lattice3 :::"complete"::: ) ($#v3_waybel_3 :::"continuous"::: ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "A")) ($#r1_waybel22 :::"is_FreeGen_set_of"::: ) (Set (Var "S")))) "holds" (Bool "for" (Set (Var "h9")) "being" ($#m1_waybel16 :::"CLHomomorphism"::: ) "of" (Set (Var "S")) "," (Set (Var "S")) "st" (Bool (Bool (Set (Set (Var "h9")) ($#k2_partfun1 :::"|"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k6_partfun1 :::"id"::: ) (Set (Var "A"))))) "holds" (Bool (Set (Var "h9")) ($#r2_funct_2 :::"="::: ) (Set ($#k3_struct_0 :::"id"::: ) (Set (Var "S"))))))) ; begin definitionlet "X" be ($#m1_hidden :::"set"::: ) ; func :::"FixedUltraFilters"::: "X" -> ($#m1_subset_1 :::"Subset-Family":::) "of" (Set "(" ($#k3_yellow_1 :::"BoolePoset"::: ) "X" ")" ) equals :: WAYBEL22:def 2 "{" (Set "(" ($#k6_waybel_0 :::"uparrow"::: ) (Set (Var "x")) ")" ) where x "is" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k3_yellow_1 :::"BoolePoset"::: ) "X" ")" ) : (Bool "ex" (Set (Var "z")) "being" ($#m1_subset_1 :::"Element"::: ) "of" "X" "st" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "z")) ($#k1_tarski :::"}"::: ) ))) "}" ; end; :: deftheorem defines :::"FixedUltraFilters"::: WAYBEL22:def 2 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k1_waybel22 :::"FixedUltraFilters"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) "{" (Set "(" ($#k6_waybel_0 :::"uparrow"::: ) (Set (Var "x")) ")" ) where x "is" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k3_yellow_1 :::"BoolePoset"::: ) (Set (Var "X")) ")" ) : (Bool "ex" (Set (Var "z")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) "st" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "z")) ($#k1_tarski :::"}"::: ) ))) "}" )); theorem :: WAYBEL22:9 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k1_waybel22 :::"FixedUltraFilters"::: ) (Set (Var "X"))) ($#r1_tarski :::"c="::: ) (Set ($#k8_waybel_0 :::"Filt"::: ) (Set "(" ($#k3_yellow_1 :::"BoolePoset"::: ) (Set (Var "X")) ")" )))) ; theorem :: WAYBEL22:10 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k1_card_1 :::"card"::: ) (Set "(" ($#k1_waybel22 :::"FixedUltraFilters"::: ) (Set (Var "X")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_card_1 :::"card"::: ) (Set (Var "X"))))) ; theorem :: WAYBEL22:11 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Filter":::) "of" (Set "(" ($#k3_yellow_1 :::"BoolePoset"::: ) (Set (Var "X")) ")" ) "holds" (Bool (Set (Var "F")) ($#r1_hidden :::"="::: ) (Set ($#k1_yellow_0 :::""\/""::: ) "(" "{" (Set "(" ($#k2_yellow_0 :::""/\""::: ) "(" "{" (Set "(" ($#k6_waybel_0 :::"uparrow"::: ) (Set (Var "x")) ")" ) where x "is" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k3_yellow_1 :::"BoolePoset"::: ) (Set (Var "X")) ")" ) : (Bool "ex" (Set (Var "z")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) "st" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "z")) ($#k1_tarski :::"}"::: ) )) & (Bool (Set (Var "z")) ($#r2_hidden :::"in"::: ) (Set (Var "Y"))) ")" )) "}" "," (Set "(" ($#k2_yellow_1 :::"InclPoset"::: ) (Set "(" ($#k8_waybel_0 :::"Filt"::: ) (Set "(" ($#k3_yellow_1 :::"BoolePoset"::: ) (Set (Var "X")) ")" ) ")" ) ")" ) ")" ")" ) where Y "is" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) : (Bool (Set (Var "Y")) ($#r2_hidden :::"in"::: ) (Set (Var "F"))) "}" "," (Set "(" ($#k2_yellow_1 :::"InclPoset"::: ) (Set "(" ($#k8_waybel_0 :::"Filt"::: ) (Set "(" ($#k3_yellow_1 :::"BoolePoset"::: ) (Set (Var "X")) ")" ) ")" ) ")" ) ")" )))) ; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_lattice3 :::"complete"::: ) ($#v3_waybel_3 :::"continuous"::: ) ($#l1_orders_2 :::"Poset":::); let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k1_waybel22 :::"FixedUltraFilters"::: ) (Set (Const "X")) ")" ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "L"))); func "f" :::"-extension_to_hom"::: -> ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k2_yellow_1 :::"InclPoset"::: ) (Set "(" ($#k8_waybel_0 :::"Filt"::: ) (Set "(" ($#k3_yellow_1 :::"BoolePoset"::: ) "X" ")" ) ")" ) ")" ) "," "L" means :: WAYBEL22:def 3 (Bool "for" (Set (Var "Fi")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k2_yellow_1 :::"InclPoset"::: ) (Set "(" ($#k8_waybel_0 :::"Filt"::: ) (Set "(" ($#k3_yellow_1 :::"BoolePoset"::: ) "X" ")" ) ")" ) ")" ) "holds" (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set (Var "Fi"))) ($#r1_hidden :::"="::: ) (Set ($#k1_yellow_0 :::""\/""::: ) "(" "{" (Set "(" ($#k2_yellow_0 :::""/\""::: ) "(" "{" (Set "(" "f" ($#k1_funct_1 :::"."::: ) (Set "(" ($#k6_waybel_0 :::"uparrow"::: ) (Set (Var "x")) ")" ) ")" ) where x "is" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k3_yellow_1 :::"BoolePoset"::: ) "X" ")" ) : (Bool "ex" (Set (Var "z")) "being" ($#m1_subset_1 :::"Element"::: ) "of" "X" "st" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "z")) ($#k1_tarski :::"}"::: ) )) & (Bool (Set (Var "z")) ($#r2_hidden :::"in"::: ) (Set (Var "Y"))) ")" )) "}" "," "L" ")" ")" ) where Y "is" ($#m1_subset_1 :::"Subset":::) "of" "X" : (Bool (Set (Var "Y")) ($#r2_hidden :::"in"::: ) (Set (Var "Fi"))) "}" "," "L" ")" ))); end; :: deftheorem defines :::"-extension_to_hom"::: WAYBEL22:def 3 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_lattice3 :::"complete"::: ) ($#v3_waybel_3 :::"continuous"::: ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k1_waybel22 :::"FixedUltraFilters"::: ) (Set (Var "X")) ")" ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L"))) (Bool "for" (Set (Var "b4")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k2_yellow_1 :::"InclPoset"::: ) (Set "(" ($#k8_waybel_0 :::"Filt"::: ) (Set "(" ($#k3_yellow_1 :::"BoolePoset"::: ) (Set (Var "X")) ")" ) ")" ) ")" ) "," (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k2_waybel22 :::"-extension_to_hom"::: ) )) "iff" (Bool "for" (Set (Var "Fi")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k2_yellow_1 :::"InclPoset"::: ) (Set "(" ($#k8_waybel_0 :::"Filt"::: ) (Set "(" ($#k3_yellow_1 :::"BoolePoset"::: ) (Set (Var "X")) ")" ) ")" ) ")" ) "holds" (Bool (Set (Set (Var "b4")) ($#k3_funct_2 :::"."::: ) (Set (Var "Fi"))) ($#r1_hidden :::"="::: ) (Set ($#k1_yellow_0 :::""\/""::: ) "(" "{" (Set "(" ($#k2_yellow_0 :::""/\""::: ) "(" "{" (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k6_waybel_0 :::"uparrow"::: ) (Set (Var "x")) ")" ) ")" ) where x "is" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k3_yellow_1 :::"BoolePoset"::: ) (Set (Var "X")) ")" ) : (Bool "ex" (Set (Var "z")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) "st" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "z")) ($#k1_tarski :::"}"::: ) )) & (Bool (Set (Var "z")) ($#r2_hidden :::"in"::: ) (Set (Var "Y"))) ")" )) "}" "," (Set (Var "L")) ")" ")" ) where Y "is" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) : (Bool (Set (Var "Y")) ($#r2_hidden :::"in"::: ) (Set (Var "Fi"))) "}" "," (Set (Var "L")) ")" ))) ")" ))))); theorem :: WAYBEL22:12 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_lattice3 :::"complete"::: ) ($#v3_waybel_3 :::"continuous"::: ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k1_waybel22 :::"FixedUltraFilters"::: ) (Set (Var "X")) ")" ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L"))) "holds" (Bool (Set (Set (Var "f")) ($#k2_waybel22 :::"-extension_to_hom"::: ) ) "is" ($#v5_orders_3 :::"monotone"::: ) )))) ; theorem :: WAYBEL22:13 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_lattice3 :::"complete"::: ) ($#v3_waybel_3 :::"continuous"::: ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k1_waybel22 :::"FixedUltraFilters"::: ) (Set (Var "X")) ")" ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L"))) "holds" (Bool (Set (Set "(" (Set (Var "f")) ($#k2_waybel22 :::"-extension_to_hom"::: ) ")" ) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k4_yellow_0 :::"Top"::: ) (Set "(" ($#k2_yellow_1 :::"InclPoset"::: ) (Set "(" ($#k8_waybel_0 :::"Filt"::: ) (Set "(" ($#k3_yellow_1 :::"BoolePoset"::: ) (Set (Var "X")) ")" ) ")" ) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_yellow_0 :::"Top"::: ) (Set (Var "L"))))))) ; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_lattice3 :::"complete"::: ) ($#v3_waybel_3 :::"continuous"::: ) ($#l1_orders_2 :::"Poset":::); let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k1_waybel22 :::"FixedUltraFilters"::: ) (Set (Const "X")) ")" ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "L"))); cluster (Set "f" ($#k2_waybel22 :::"-extension_to_hom"::: ) ) -> ($#v22_waybel_0 :::"directed-sups-preserving"::: ) ; end; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_lattice3 :::"complete"::: ) ($#v3_waybel_3 :::"continuous"::: ) ($#l1_orders_2 :::"Poset":::); let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k1_waybel22 :::"FixedUltraFilters"::: ) (Set (Const "X")) ")" ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "L"))); cluster (Set "f" ($#k2_waybel22 :::"-extension_to_hom"::: ) ) -> ($#v17_waybel_0 :::"infs-preserving"::: ) ; end; theorem :: WAYBEL22:14 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_lattice3 :::"complete"::: ) ($#v3_waybel_3 :::"continuous"::: ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k1_waybel22 :::"FixedUltraFilters"::: ) (Set (Var "X")) ")" ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L"))) "holds" (Bool (Set (Set "(" (Set (Var "f")) ($#k2_waybel22 :::"-extension_to_hom"::: ) ")" ) ($#k2_partfun1 :::"|"::: ) (Set "(" ($#k1_waybel22 :::"FixedUltraFilters"::: ) (Set (Var "X")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "f")))))) ; theorem :: WAYBEL22:15 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_lattice3 :::"complete"::: ) ($#v3_waybel_3 :::"continuous"::: ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k1_waybel22 :::"FixedUltraFilters"::: ) (Set (Var "X")) ")" ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L"))) (Bool "for" (Set (Var "h")) "being" ($#m1_waybel16 :::"CLHomomorphism"::: ) "of" (Set ($#k2_yellow_1 :::"InclPoset"::: ) (Set "(" ($#k8_waybel_0 :::"Filt"::: ) (Set "(" ($#k3_yellow_1 :::"BoolePoset"::: ) (Set (Var "X")) ")" ) ")" )) "," (Set (Var "L")) "st" (Bool (Bool (Set (Set (Var "h")) ($#k2_partfun1 :::"|"::: ) (Set "(" ($#k1_waybel22 :::"FixedUltraFilters"::: ) (Set (Var "X")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "f")))) "holds" (Bool (Set (Var "h")) ($#r2_funct_2 :::"="::: ) (Set (Set (Var "f")) ($#k2_waybel22 :::"-extension_to_hom"::: ) )))))) ; theorem :: WAYBEL22:16 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k1_waybel22 :::"FixedUltraFilters"::: ) (Set (Var "X"))) ($#r1_waybel22 :::"is_FreeGen_set_of"::: ) (Set ($#k2_yellow_1 :::"InclPoset"::: ) (Set "(" ($#k8_waybel_0 :::"Filt"::: ) (Set "(" ($#k3_yellow_1 :::"BoolePoset"::: ) (Set (Var "X")) ")" ) ")" )))) ; theorem :: WAYBEL22:17 (Bool "for" (Set (Var "L")) "," (Set (Var "M")) "being" ($#v3_lattice3 :::"complete"::: ) ($#v3_waybel_3 :::"continuous"::: ) ($#l1_orders_2 :::"LATTICE":::) (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "F")) ($#r1_waybel22 :::"is_FreeGen_set_of"::: ) (Set (Var "L"))) & (Bool (Set (Var "G")) ($#r1_waybel22 :::"is_FreeGen_set_of"::: ) (Set (Var "M"))) & (Bool (Set ($#k1_card_1 :::"card"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set ($#k1_card_1 :::"card"::: ) (Set (Var "G"))))) "holds" (Bool (Set (Var "L")) "," (Set (Var "M")) ($#r5_waybel_1 :::"are_isomorphic"::: ) ))) ; theorem :: WAYBEL22:18 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "L")) "being" ($#v3_lattice3 :::"complete"::: ) ($#v3_waybel_3 :::"continuous"::: ) ($#l1_orders_2 :::"LATTICE":::) (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "G")) ($#r1_waybel22 :::"is_FreeGen_set_of"::: ) (Set (Var "L"))) & (Bool (Set ($#k1_card_1 :::"card"::: ) (Set (Var "G"))) ($#r1_hidden :::"="::: ) (Set ($#k1_card_1 :::"card"::: ) (Set (Var "X"))))) "holds" (Bool (Set (Var "L")) "," (Set ($#k2_yellow_1 :::"InclPoset"::: ) (Set "(" ($#k8_waybel_0 :::"Filt"::: ) (Set "(" ($#k3_yellow_1 :::"BoolePoset"::: ) (Set (Var "X")) ")" ) ")" )) ($#r5_waybel_1 :::"are_isomorphic"::: ) )))) ;