:: YELLOW16  semantic presentation begin  
theorem :: YELLOW16:1 canceled; 
 
theorem :: YELLOW16:2 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "L")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "S")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#m1_yellow_0 :::"SubRelStr"::: )   "of" (Set (Var "L"))  (Bool  "for" (Set (Var "f")) "," (Set (Var "g")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "S")))  (Bool  "for" (Set (Var "f9")) "," (Set (Var "g9")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "L")))  "st" (Bool (Bool (Set (Var "f9"))  ($#r1_funct_2 :::"="::: )  (Set (Var "f"))) & (Bool (Set (Var "g9"))  ($#r1_funct_2 :::"="::: )  (Set (Var "g"))) & (Bool (Set (Var "f"))  ($#r1_yellow_2 :::"<="::: )  (Set (Var "g")))) "holds"  (Bool (Set (Var "f9"))  ($#r1_yellow_2 :::"<="::: )  (Set (Var "g9")))))))) ; 
 
theorem :: YELLOW16:3 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "L")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "S")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v4_yellow_0 :::"full"::: )     ($#m1_yellow_0 :::"SubRelStr"::: )   "of" (Set (Var "L"))  (Bool  "for" (Set (Var "f")) "," (Set (Var "g")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "S")))  (Bool  "for" (Set (Var "f9")) "," (Set (Var "g9")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "L")))  "st" (Bool (Bool (Set (Var "f9"))  ($#r1_funct_2 :::"="::: )  (Set (Var "f"))) & (Bool (Set (Var "g9"))  ($#r1_funct_2 :::"="::: )  (Set (Var "g"))) & (Bool (Set (Var "f9"))  ($#r1_yellow_2 :::"<="::: )  (Set (Var "g9")))) "holds"  (Bool (Set (Var "f"))  ($#r1_yellow_2 :::"<="::: )  (Set (Var "g")))))))) ; 
 registrationlet "S" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_orders_2 :::"RelStr"::: )  ; let "T" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v3_orders_2 :::"reflexive"::: )     ($#v5_orders_2 :::"antisymmetric"::: )     ($#l1_orders_2 :::"RelStr"::: )  ; 
cluster   ($#v1_relat_1 :::"Relation-like"::: )   (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "S")  ($#v4_relat_1 :::"-defined"::: )   (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "T")  ($#v5_relat_1 :::"-valued"::: )     ($#v1_funct_1 :::"Function-like"::: )    ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )  bbbadV1_PARTFUN1((Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "S"))   ($#v1_funct_2 :::"quasi_total"::: )     ($#v5_orders_3 :::"monotone"::: )     ($#v22_waybel_0 :::"directed-sups-preserving"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (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 :: YELLOW16:4 (Bool  "for" (Set (Var "f")) "," (Set (Var "g")) "being"   ($#m1_hidden :::"Function":::)  "st" (Bool (Bool (Set (Var "f")) "is"   ($#v11_quantal1 :::"idempotent"::: )  ) & (Bool (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "g")))  ($#r1_tarski :::"c="::: )  (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "f")))) & (Bool (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "g")))  ($#r1_tarski :::"c="::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "f"))))) "holds"  (Bool (Set (Set (Var "f"))  ($#k3_relat_1 :::"*"::: )  (Set (Var "g")))  ($#r1_hidden :::"="::: )  (Set (Var "g")))) ; 
 registrationlet "S" be    ($#l1_struct_0 :::"1-sorted"::: )  ; 
cluster   ($#v1_relat_1 :::"Relation-like"::: )   (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "S")  ($#v4_relat_1 :::"-defined"::: )   (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "S")  ($#v5_relat_1 :::"-valued"::: )     ($#v1_funct_1 :::"Function-like"::: )   bbbadV1_PARTFUN1((Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "S"))   ($#v1_funct_2 :::"quasi_total"::: )     ($#v11_quantal1 :::"idempotent"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_zfmisc_1 :::"bool"::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "S") "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "S") ($#k2_zfmisc_1 :::":]"::: ) )); 
end; 
theorem :: YELLOW16:5 (Bool  "for" (Set (Var "L")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v24_waybel_0 :::"up-complete"::: )    ($#l1_orders_2 :::"Poset":::)  (Bool  "for" (Set (Var "S")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v4_yellow_0 :::"full"::: )     ($#v4_waybel_0 :::"directed-sups-inheriting"::: )     ($#m1_yellow_0 :::"SubRelStr"::: )   "of" (Set (Var "L")) "holds"  (Bool (Set (Var "S")) "is"   ($#v24_waybel_0 :::"up-complete"::: )  ))) ; 
 
theorem :: YELLOW16:6 (Bool  "for" (Set (Var "L")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v24_waybel_0 :::"up-complete"::: )    ($#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"::: )  ) & (Bool (Set (Var "f")) "is"   ($#v22_waybel_0 :::"directed-sups-preserving"::: )  )) "holds"  (Bool (Set   ($#k1_yellow_2 :::"Image"::: )  (Set (Var "f"))) "is"   ($#v4_waybel_0 :::"directed-sups-inheriting"::: )  ))) ; 
 
theorem :: YELLOW16:7 (Bool  "for" (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "S")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#m1_yellow_0 :::"SubRelStr"::: )   "of" (Set (Var "T"))  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "T")) "," (Set (Var "S"))  "st" (Bool (Bool (Set (Set (Var "f"))  ($#k1_partfun1 :::"*"::: )  (Set  "("  ($#k1_yellow_9 :::"incl"::: )   "(" (Set (Var "S")) "," (Set (Var "T")) ")"  ")" ))  ($#r2_funct_2 :::"="::: )  (Set   ($#k3_struct_0 :::"id"::: )  (Set (Var "S"))))) "holds"  (Bool (Set (Var "f")) "is"   ($#v11_quantal1 :::"idempotent"::: )    ($#m1_subset_1 :::"Function":::) "of" (Set (Var "T")) "," (Set (Var "T")))))) ; 
 definitionlet "S", "T" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_orders_2 :::"Poset":::); let "f" be   ($#m1_hidden :::"Function":::); pred "f" :::"is_a_retraction_of"::: "T" "," "S" means :: YELLOW16:def 1 (Bool  "("  (Bool "f" "is"   ($#v22_waybel_0 :::"directed-sups-preserving"::: )    ($#m1_subset_1 :::"Function":::) "of" "T" "," "S") & (Bool (Set "f"  ($#k5_relat_1 :::"|"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "S"))  ($#r1_hidden :::"="::: )  (Set   ($#k3_struct_0 :::"id"::: )  "S")) & (Bool "S" "is"   ($#v4_yellow_0 :::"full"::: )     ($#v4_waybel_0 :::"directed-sups-inheriting"::: )     ($#m1_yellow_0 :::"SubRelStr"::: )   "of" "T")  ")" ); pred "f" :::"is_an_UPS_retraction_of"::: "T" "," "S" means :: YELLOW16:def 2 (Bool  "("  (Bool "f" "is"   ($#v22_waybel_0 :::"directed-sups-preserving"::: )    ($#m1_subset_1 :::"Function":::) "of" "T" "," "S") & (Bool  "ex" (Set (Var "g")) "being"   ($#v22_waybel_0 :::"directed-sups-preserving"::: )    ($#m1_subset_1 :::"Function":::) "of" "S" "," "T" "st" (Bool (Set "f"  ($#k3_relat_1 :::"*"::: )  (Set (Var "g")))  ($#r1_hidden :::"="::: )  (Set   ($#k3_struct_0 :::"id"::: )  "S")))  ")" ); end; 












:: deftheorem    defines :::"is_a_retraction_of"::: YELLOW16:def 1 :  (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 "f")) "being"   ($#m1_hidden :::"Function":::) "holds"   (Bool  "("  (Bool (Set (Var "f"))  ($#r1_yellow16 :::"is_a_retraction_of"::: )  (Set (Var "T")) "," (Set (Var "S"))) "iff" (Bool  "("  (Bool (Set (Var "f")) "is"   ($#v22_waybel_0 :::"directed-sups-preserving"::: )    ($#m1_subset_1 :::"Function":::) "of" (Set (Var "T")) "," (Set (Var "S"))) & (Bool (Set (Set (Var "f"))  ($#k5_relat_1 :::"|"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "S"))))  ($#r1_hidden :::"="::: )  (Set   ($#k3_struct_0 :::"id"::: )  (Set (Var "S")))) & (Bool (Set (Var "S")) "is"   ($#v4_yellow_0 :::"full"::: )     ($#v4_waybel_0 :::"directed-sups-inheriting"::: )     ($#m1_yellow_0 :::"SubRelStr"::: )   "of" (Set (Var "T")))  ")" )  ")" ))); 
 
:: deftheorem    defines :::"is_an_UPS_retraction_of"::: YELLOW16:def 2 :  (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 "f")) "being"   ($#m1_hidden :::"Function":::) "holds"   (Bool  "("  (Bool (Set (Var "f"))  ($#r2_yellow16 :::"is_an_UPS_retraction_of"::: )  (Set (Var "T")) "," (Set (Var "S"))) "iff" (Bool  "("  (Bool (Set (Var "f")) "is"   ($#v22_waybel_0 :::"directed-sups-preserving"::: )    ($#m1_subset_1 :::"Function":::) "of" (Set (Var "T")) "," (Set (Var "S"))) & (Bool  "ex" (Set (Var "g")) "being"   ($#v22_waybel_0 :::"directed-sups-preserving"::: )    ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set (Var "T")) "st" (Bool (Set (Set (Var "f"))  ($#k3_relat_1 :::"*"::: )  (Set (Var "g")))  ($#r1_hidden :::"="::: )  (Set   ($#k3_struct_0 :::"id"::: )  (Set (Var "S")))))  ")" )  ")" ))); 
 definitionlet "S", "T" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_orders_2 :::"Poset":::); pred "S" :::"is_a_retract_of"::: "T" means :: YELLOW16:def 3 (Bool  "ex" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" "T" "," "S" "st" (Bool (Set (Var "f"))  ($#r1_yellow16 :::"is_a_retraction_of"::: )  "T" "," "S")); pred "S" :::"is_an_UPS_retract_of"::: "T" means :: YELLOW16:def 4 (Bool  "ex" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" "T" "," "S" "st" (Bool (Set (Var "f"))  ($#r2_yellow16 :::"is_an_UPS_retraction_of"::: )  "T" "," "S")); end; 










:: deftheorem    defines :::"is_a_retract_of"::: YELLOW16:def 3 :  (Bool  "for" (Set (Var "S")) "," (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_orders_2 :::"Poset":::) "holds"   (Bool  "("  (Bool (Set (Var "S"))  ($#r3_yellow16 :::"is_a_retract_of"::: )  (Set (Var "T"))) "iff" (Bool  "ex" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "T")) "," (Set (Var "S")) "st" (Bool (Set (Var "f"))  ($#r1_yellow16 :::"is_a_retraction_of"::: )  (Set (Var "T")) "," (Set (Var "S"))))  ")" )); 
 
:: deftheorem    defines :::"is_an_UPS_retract_of"::: YELLOW16:def 4 :  (Bool  "for" (Set (Var "S")) "," (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_orders_2 :::"Poset":::) "holds"   (Bool  "("  (Bool (Set (Var "S"))  ($#r4_yellow16 :::"is_an_UPS_retract_of"::: )  (Set (Var "T"))) "iff" (Bool  "ex" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "T")) "," (Set (Var "S")) "st" (Bool (Set (Var "f"))  ($#r2_yellow16 :::"is_an_UPS_retraction_of"::: )  (Set (Var "T")) "," (Set (Var "S"))))  ")" )); 
 
theorem :: YELLOW16: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 "f")) "being"   ($#m1_hidden :::"Function":::)  "st" (Bool (Bool (Set (Var "f"))  ($#r1_yellow16 :::"is_a_retraction_of"::: )  (Set (Var "T")) "," (Set (Var "S")))) "holds"  (Bool (Set (Set (Var "f"))  ($#k3_relat_1 :::"*"::: )  (Set  "("  ($#k1_yellow_9 :::"incl"::: )   "(" (Set (Var "S")) "," (Set (Var "T")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k3_struct_0 :::"id"::: )  (Set (Var "S")))))) ; 
 
theorem :: YELLOW16:9 (Bool  "for" (Set (Var "S")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_orders_2 :::"Poset":::)  (Bool  "for" (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v24_waybel_0 :::"up-complete"::: )    ($#l1_orders_2 :::"Poset":::)  (Bool  "for" (Set (Var "f")) "being"   ($#m1_hidden :::"Function":::)  "st" (Bool (Bool (Set (Var "f"))  ($#r1_yellow16 :::"is_a_retraction_of"::: )  (Set (Var "T")) "," (Set (Var "S")))) "holds"  (Bool (Set (Var "f"))  ($#r2_yellow16 :::"is_an_UPS_retraction_of"::: )  (Set (Var "T")) "," (Set (Var "S")))))) ; 
 
theorem :: YELLOW16: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 "f")) "being"   ($#m1_hidden :::"Function":::)  "st" (Bool (Bool (Set (Var "f"))  ($#r1_yellow16 :::"is_a_retraction_of"::: )  (Set (Var "T")) "," (Set (Var "S")))) "holds"  (Bool (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "f")))  ($#r1_hidden :::"="::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "S")))))) ; 
 
theorem :: YELLOW16: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 "f")) "being"   ($#m1_hidden :::"Function":::)  "st" (Bool (Bool (Set (Var "f"))  ($#r2_yellow16 :::"is_an_UPS_retraction_of"::: )  (Set (Var "T")) "," (Set (Var "S")))) "holds"  (Bool (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "f")))  ($#r1_hidden :::"="::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "S")))))) ; 
 
theorem :: YELLOW16: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 "f")) "being"   ($#m1_hidden :::"Function":::)  "st" (Bool (Bool (Set (Var "f"))  ($#r1_yellow16 :::"is_a_retraction_of"::: )  (Set (Var "T")) "," (Set (Var "S")))) "holds"  (Bool (Set (Var "f")) "is"   ($#v11_quantal1 :::"idempotent"::: )    ($#m1_subset_1 :::"Function":::) "of" (Set (Var "T")) "," (Set (Var "T"))))) ; 
 
theorem :: YELLOW16:13 (Bool  "for" (Set (Var "T")) "," (Set (Var "S")) "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 "T")) "," (Set (Var "T"))  "st" (Bool (Bool (Set (Var "f"))  ($#r1_yellow16 :::"is_a_retraction_of"::: )  (Set (Var "T")) "," (Set (Var "S")))) "holds"  (Bool (Set   ($#k1_yellow_2 :::"Image"::: )  (Set (Var "f")))  ($#r1_hidden :::"="::: )  (Set   ($#g1_orders_2 :::"RelStr"::: )  "(#"  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "S"))) "," (Set  "the"  ($#u1_orders_2 :::"InternalRel"::: )  "of" (Set (Var "S"))) "#)" )))) ; 
 
theorem :: YELLOW16:14 (Bool  "for" (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v24_waybel_0 :::"up-complete"::: )    ($#l1_orders_2 :::"Poset":::)  (Bool  "for" (Set (Var "S")) "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 "T")) "," (Set (Var "T"))  "st" (Bool (Bool (Set (Var "f"))  ($#r1_yellow16 :::"is_a_retraction_of"::: )  (Set (Var "T")) "," (Set (Var "S")))) "holds"  (Bool  "("  (Bool (Set (Var "f")) "is"   ($#v22_waybel_0 :::"directed-sups-preserving"::: )  ) & (Bool (Set (Var "f")) "is"   ($#v6_waybel_1 :::"projection"::: )  )  ")" )))) ; 
 
theorem :: YELLOW16:15 (Bool  "for" (Set (Var "S")) "," (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v3_orders_2 :::"reflexive"::: )     ($#v4_orders_2 :::"transitive"::: )     ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set (Var "T")) "holds"   (Bool  "("  (Bool (Set (Var "f")) "is"   ($#v23_waybel_0 :::"isomorphic"::: )  ) "iff" (Bool  "("  (Bool (Set (Var "f")) "is"   ($#v5_orders_3 :::"monotone"::: )  ) & (Bool  "ex" (Set (Var "g")) "being"   ($#v5_orders_3 :::"monotone"::: )    ($#m1_subset_1 :::"Function":::) "of" (Set (Var "T")) "," (Set (Var "S")) "st"  (Bool  "("  (Bool (Set (Set (Var "f"))  ($#k1_partfun1 :::"*"::: )  (Set (Var "g")))  ($#r2_funct_2 :::"="::: )  (Set   ($#k3_struct_0 :::"id"::: )  (Set (Var "T")))) & (Bool (Set (Set (Var "g"))  ($#k1_partfun1 :::"*"::: )  (Set (Var "f")))  ($#r2_funct_2 :::"="::: )  (Set   ($#k3_struct_0 :::"id"::: )  (Set (Var "S"))))  ")" ))  ")" )  ")" ))) ; 
 
theorem :: YELLOW16:16 (Bool  "for" (Set (Var "S")) "," (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_orders_2 :::"Poset":::) "holds"   (Bool  "("  (Bool (Set (Var "S")) "," (Set (Var "T"))  ($#r5_waybel_1 :::"are_isomorphic"::: )  ) "iff" (Bool  "ex" (Set (Var "f")) "being"   ($#v5_orders_3 :::"monotone"::: )    ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set (Var "T"))(Bool  "ex" (Set (Var "g")) "being"   ($#v5_orders_3 :::"monotone"::: )    ($#m1_subset_1 :::"Function":::) "of" (Set (Var "T")) "," (Set (Var "S")) "st"  (Bool  "("  (Bool (Set (Set (Var "f"))  ($#k1_partfun1 :::"*"::: )  (Set (Var "g")))  ($#r2_funct_2 :::"="::: )  (Set   ($#k3_struct_0 :::"id"::: )  (Set (Var "T")))) & (Bool (Set (Set (Var "g"))  ($#k1_partfun1 :::"*"::: )  (Set (Var "f")))  ($#r2_funct_2 :::"="::: )  (Set   ($#k3_struct_0 :::"id"::: )  (Set (Var "S"))))  ")" )))  ")" )) ; 
 
theorem :: YELLOW16:17 (Bool  "for" (Set (Var "S")) "," (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v24_waybel_0 :::"up-complete"::: )    ($#l1_orders_2 :::"Poset":::)  "st" (Bool (Bool (Set (Var "S")) "," (Set (Var "T"))  ($#r5_waybel_1 :::"are_isomorphic"::: )  )) "holds"  (Bool  "("  (Bool (Set (Var "S"))  ($#r4_yellow16 :::"is_an_UPS_retract_of"::: )  (Set (Var "T"))) & (Bool (Set (Var "T"))  ($#r4_yellow16 :::"is_an_UPS_retract_of"::: )  (Set (Var "S")))  ")" )) ; 
 
theorem :: YELLOW16:18 (Bool  "for" (Set (Var "T")) "," (Set (Var "S")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_orders_2 :::"Poset":::)  (Bool  "for" (Set (Var "f")) "being"   ($#v5_orders_3 :::"monotone"::: )    ($#m1_subset_1 :::"Function":::) "of" (Set (Var "T")) "," (Set (Var "S"))  (Bool  "for" (Set (Var "g")) "being"   ($#v5_orders_3 :::"monotone"::: )    ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set (Var "T"))  "st" (Bool (Bool (Set (Set (Var "f"))  ($#k1_partfun1 :::"*"::: )  (Set (Var "g")))  ($#r2_funct_2 :::"="::: )  (Set   ($#k3_struct_0 :::"id"::: )  (Set (Var "S"))))) "holds"  (Bool  "ex" (Set (Var "h")) "being"   ($#v6_waybel_1 :::"projection"::: )    ($#m1_subset_1 :::"Function":::) "of" (Set (Var "T")) "," (Set (Var "T")) "st"  (Bool  "("  (Bool (Set (Var "h"))  ($#r2_funct_2 :::"="::: )  (Set (Set (Var "g"))  ($#k1_partfun1 :::"*"::: )  (Set (Var "f")))) & (Bool (Set (Set (Var "h"))  ($#k2_partfun1 :::"|"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set  "("  ($#k1_yellow_2 :::"Image"::: )  (Set (Var "h")) ")" )))  ($#r1_hidden :::"="::: )  (Set   ($#k3_struct_0 :::"id"::: )  (Set  "("  ($#k1_yellow_2 :::"Image"::: )  (Set (Var "h")) ")" ))) & (Bool (Set (Var "S")) "," (Set   ($#k1_yellow_2 :::"Image"::: )  (Set (Var "h")))  ($#r5_waybel_1 :::"are_isomorphic"::: )  )  ")" ))))) ; 
 
theorem :: YELLOW16:19 (Bool  "for" (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v24_waybel_0 :::"up-complete"::: )    ($#l1_orders_2 :::"Poset":::)  (Bool  "for" (Set (Var "S")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_orders_2 :::"Poset":::)  (Bool  "for" (Set (Var "f")) "being"   ($#m1_hidden :::"Function":::)  "st" (Bool (Bool (Set (Var "f"))  ($#r2_yellow16 :::"is_an_UPS_retraction_of"::: )  (Set (Var "T")) "," (Set (Var "S")))) "holds"  (Bool  "ex" (Set (Var "h")) "being"   ($#v22_waybel_0 :::"directed-sups-preserving"::: )     ($#v6_waybel_1 :::"projection"::: )    ($#m1_subset_1 :::"Function":::) "of" (Set (Var "T")) "," (Set (Var "T")) "st"  (Bool  "("  (Bool (Set (Var "h"))  ($#r1_yellow16 :::"is_a_retraction_of"::: )  (Set (Var "T")) "," (Set   ($#k1_yellow_2 :::"Image"::: )  (Set (Var "h")))) & (Bool (Set (Var "S")) "," (Set   ($#k1_yellow_2 :::"Image"::: )  (Set (Var "h")))  ($#r5_waybel_1 :::"are_isomorphic"::: )  )  ")" ))))) ; 
 
theorem :: YELLOW16:20 (Bool  "for" (Set (Var "L")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v24_waybel_0 :::"up-complete"::: )    ($#l1_orders_2 :::"Poset":::)  (Bool  "for" (Set (Var "S")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_orders_2 :::"Poset":::)  "st" (Bool (Bool (Set (Var "S"))  ($#r3_yellow16 :::"is_a_retract_of"::: )  (Set (Var "L")))) "holds"  (Bool (Set (Var "S")) "is"   ($#v24_waybel_0 :::"up-complete"::: )  ))) ; 
 
theorem :: YELLOW16:21 (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 "S")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_orders_2 :::"Poset":::)  "st" (Bool (Bool (Set (Var "S"))  ($#r3_yellow16 :::"is_a_retract_of"::: )  (Set (Var "L")))) "holds"  (Bool (Set (Var "S")) "is"   ($#v3_lattice3 :::"complete"::: )  ))) ; 
 
theorem :: YELLOW16:22 (Bool  "for" (Set (Var "L")) "being"   ($#v3_lattice3 :::"complete"::: )     ($#v3_waybel_3 :::"continuous"::: )    ($#l1_orders_2 :::"LATTICE":::)  (Bool  "for" (Set (Var "S")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_orders_2 :::"Poset":::)  "st" (Bool (Bool (Set (Var "S"))  ($#r3_yellow16 :::"is_a_retract_of"::: )  (Set (Var "L")))) "holds"  (Bool (Set (Var "S")) "is"   ($#v3_waybel_3 :::"continuous"::: )  ))) ; 
 
theorem :: YELLOW16:23 (Bool  "for" (Set (Var "L")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v24_waybel_0 :::"up-complete"::: )    ($#l1_orders_2 :::"Poset":::)  (Bool  "for" (Set (Var "S")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_orders_2 :::"Poset":::)  "st" (Bool (Bool (Set (Var "S"))  ($#r4_yellow16 :::"is_an_UPS_retract_of"::: )  (Set (Var "L")))) "holds"  (Bool (Set (Var "S")) "is"   ($#v24_waybel_0 :::"up-complete"::: )  ))) ; 
 
theorem :: YELLOW16:24 (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 "S")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_orders_2 :::"Poset":::)  "st" (Bool (Bool (Set (Var "S"))  ($#r4_yellow16 :::"is_an_UPS_retract_of"::: )  (Set (Var "L")))) "holds"  (Bool (Set (Var "S")) "is"   ($#v3_lattice3 :::"complete"::: )  ))) ; 
 
theorem :: YELLOW16:25 (Bool  "for" (Set (Var "L")) "being"   ($#v3_lattice3 :::"complete"::: )     ($#v3_waybel_3 :::"continuous"::: )    ($#l1_orders_2 :::"LATTICE":::)  (Bool  "for" (Set (Var "S")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_orders_2 :::"Poset":::)  "st" (Bool (Bool (Set (Var "S"))  ($#r4_yellow16 :::"is_an_UPS_retract_of"::: )  (Set (Var "L")))) "holds"  (Bool (Set (Var "S")) "is"   ($#v3_waybel_3 :::"continuous"::: )  ))) ; 
 
theorem :: YELLOW16:26 (Bool  "for" (Set (Var "L")) "being"    ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "S")) "being"   ($#v4_yellow_0 :::"full"::: )     ($#m1_yellow_0 :::"SubRelStr"::: )   "of" (Set (Var "L"))  (Bool  "for" (Set (Var "R")) "being"    ($#m1_yellow_0 :::"SubRelStr"::: )   "of" (Set (Var "S")) "holds"   (Bool  "("  (Bool (Set (Var "R")) "is"   ($#v4_yellow_0 :::"full"::: )  ) "iff" (Bool (Set (Var "R")) "is"   ($#v4_yellow_0 :::"full"::: )     ($#m1_yellow_0 :::"SubRelStr"::: )   "of" (Set (Var "L")))  ")" )))) ; 
 
theorem :: YELLOW16:27 (Bool  "for" (Set (Var "L")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v4_orders_2 :::"transitive"::: )     ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "S")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v4_yellow_0 :::"full"::: )     ($#v4_waybel_0 :::"directed-sups-inheriting"::: )     ($#m1_yellow_0 :::"SubRelStr"::: )   "of" (Set (Var "L"))  (Bool  "for" (Set (Var "R")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v4_waybel_0 :::"directed-sups-inheriting"::: )     ($#m1_yellow_0 :::"SubRelStr"::: )   "of" (Set (Var "S")) "holds"  (Bool (Set (Var "R")) "is"   ($#v4_waybel_0 :::"directed-sups-inheriting"::: )     ($#m1_yellow_0 :::"SubRelStr"::: )   "of" (Set (Var "L")))))) ; 
 
theorem :: YELLOW16:28 (Bool  "for" (Set (Var "L")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v24_waybel_0 :::"up-complete"::: )    ($#l1_orders_2 :::"Poset":::)  (Bool  "for" (Set (Var "S1")) "," (Set (Var "S2")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v4_yellow_0 :::"full"::: )     ($#v4_waybel_0 :::"directed-sups-inheriting"::: )     ($#m1_yellow_0 :::"SubRelStr"::: )   "of" (Set (Var "L"))  "st" (Bool (Bool (Set (Var "S1")) "is"    ($#m1_yellow_0 :::"SubRelStr"::: )   "of" (Set (Var "S2")))) "holds"  (Bool (Set (Var "S1")) "is"   ($#v4_yellow_0 :::"full"::: )     ($#v4_waybel_0 :::"directed-sups-inheriting"::: )     ($#m1_yellow_0 :::"SubRelStr"::: )   "of" (Set (Var "S2"))))) ; 
 begin  definitionlet "R" be   ($#m1_hidden :::"Relation":::); attr "R" is  :::"Poset-yielding":::  means :: YELLOW16:def 5 (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k10_xtuple_0 :::"rng"::: )  "R"))) "holds"  (Bool (Set (Var "x")) "is"   ($#l1_orders_2 :::"Poset":::))); end; 




:: deftheorem    defines :::"Poset-yielding"::: YELLOW16:def 5 :  (Bool  "for" (Set (Var "R")) "being"   ($#m1_hidden :::"Relation":::) "holds"   (Bool  "("  (Bool (Set (Var "R")) "is"   ($#v1_yellow16 :::"Poset-yielding"::: )  ) "iff" (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "R"))))) "holds"  (Bool (Set (Var "x")) "is"   ($#l1_orders_2 :::"Poset":::)))  ")" )); 
 registration
cluster   ($#v1_relat_1 :::"Relation-like"::: )     ($#v1_yellow16 :::"Poset-yielding"::: )    ->   ($#v1_yellow_1 :::"RelStr-yielding"::: )     ($#v5_waybel_3 :::"reflexive-yielding"::: )    for    ($#m1_hidden :::"set"::: )  ; 
end; definitionlet "X" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  ; let "L" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_orders_2 :::"RelStr"::: )  ; let "i" be    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Const "X")); let "Y" be   ($#m1_subset_1 :::"Subset":::) "of" (Set  "(" (Set (Const "L"))  ($#k6_yellow_1 :::"|^"::: )  (Set (Const "X")) ")" ); :: original: :::"pi"::: redefine func  :::"pi":::  "(" "Y" "," "i" ")"  ->   ($#m1_subset_1 :::"Subset":::) "of" "L"; end; registrationlet "X" be    ($#m1_hidden :::"set"::: )  ; let "S" be   ($#l1_orders_2 :::"Poset":::); 
cluster (Set "X"  ($#k2_funcop_1 :::"-->"::: )  "S") ->   ($#v1_yellow16 :::"Poset-yielding"::: )   ; 
end; registrationlet "I" be    ($#m1_hidden :::"set"::: )  ; 
cluster   ($#v1_relat_1 :::"Relation-like"::: )   "I"  ($#v4_relat_1 :::"-defined"::: )     ($#v1_funct_1 :::"Function-like"::: )   bbbadV1_PARTFUN1("I")   ($#v4_waybel_3 :::"non-Empty"::: )     ($#v1_yellow16 :::"Poset-yielding"::: )    for    ($#m1_hidden :::"set"::: )  ; 
end; registrationlet "I" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  ; let "J" be   ($#v4_waybel_3 :::"non-Empty"::: )     ($#v1_yellow16 :::"Poset-yielding"::: )    ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I")); 
cluster (Set   ($#k5_yellow_1 :::"product"::: )  "J") ->   ($#v4_orders_2 :::"transitive"::: )     ($#v5_orders_2 :::"antisymmetric"::: )   ; 
end; definitionlet "I" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  ; let "J" be   ($#v4_waybel_3 :::"non-Empty"::: )     ($#v1_yellow16 :::"Poset-yielding"::: )    ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I")); let "i" be    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Const "I")); :: original: :::"."::: redefine func "J" :::"."::: "i" ->  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_orders_2 :::"Poset":::); end; 
theorem :: YELLOW16:29 (Bool  "for" (Set (Var "I")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "J")) "being"   ($#v4_waybel_3 :::"non-Empty"::: )     ($#v1_yellow16 :::"Poset-yielding"::: )    ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I"))  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set  "("  ($#k5_yellow_1 :::"product"::: )  (Set (Var "J")) ")" )  (Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k5_yellow_1 :::"product"::: )  (Set (Var "J")) ")" ) "holds"   (Bool  "("  (Bool (Set (Var "f"))  ($#r2_lattice3 :::"is_>=_than"::: )  (Set (Var "X"))) "iff" (Bool  "for" (Set (Var "i")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "I")) "holds"  (Bool (Set (Set (Var "f"))  ($#k4_waybel_3 :::"."::: )  (Set (Var "i")))  ($#r2_lattice3 :::"is_>=_than"::: )  (Set   ($#k5_waybel_3 :::"pi"::: )   "(" (Set (Var "X")) "," (Set (Var "i")) ")" )))  ")" ))))) ; 
 
theorem :: YELLOW16:30 (Bool  "for" (Set (Var "I")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "J")) "being"   ($#v4_waybel_3 :::"non-Empty"::: )     ($#v1_yellow16 :::"Poset-yielding"::: )    ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I"))  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set  "("  ($#k5_yellow_1 :::"product"::: )  (Set (Var "J")) ")" )  (Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k5_yellow_1 :::"product"::: )  (Set (Var "J")) ")" ) "holds"   (Bool  "("  (Bool (Set (Var "f"))  ($#r1_lattice3 :::"is_<=_than"::: )  (Set (Var "X"))) "iff" (Bool  "for" (Set (Var "i")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "I")) "holds"  (Bool (Set (Set (Var "f"))  ($#k4_waybel_3 :::"."::: )  (Set (Var "i")))  ($#r1_lattice3 :::"is_<=_than"::: )  (Set   ($#k5_waybel_3 :::"pi"::: )   "(" (Set (Var "X")) "," (Set (Var "i")) ")" )))  ")" ))))) ; 
 
theorem :: YELLOW16:31 (Bool  "for" (Set (Var "I")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "J")) "being"   ($#v4_waybel_3 :::"non-Empty"::: )     ($#v1_yellow16 :::"Poset-yielding"::: )    ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I"))  (Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k5_yellow_1 :::"product"::: )  (Set (Var "J")) ")" ) "holds"   (Bool  "("  (Bool   ($#r1_yellow_0 :::"ex_sup_of"::: )  (Set (Var "X")) "," (Set   ($#k5_yellow_1 :::"product"::: )  (Set (Var "J")))) "iff" (Bool  "for" (Set (Var "i")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "I")) "holds"  (Bool   ($#r1_yellow_0 :::"ex_sup_of"::: )  (Set   ($#k5_waybel_3 :::"pi"::: )   "(" (Set (Var "X")) "," (Set (Var "i")) ")" ) "," (Set (Set (Var "J"))  ($#k2_yellow16 :::"."::: )  (Set (Var "i")))))  ")" )))) ; 
 
theorem :: YELLOW16:32 (Bool  "for" (Set (Var "I")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "J")) "being"   ($#v4_waybel_3 :::"non-Empty"::: )     ($#v1_yellow16 :::"Poset-yielding"::: )    ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I"))  (Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k5_yellow_1 :::"product"::: )  (Set (Var "J")) ")" ) "holds"   (Bool  "("  (Bool   ($#r2_yellow_0 :::"ex_inf_of"::: )  (Set (Var "X")) "," (Set   ($#k5_yellow_1 :::"product"::: )  (Set (Var "J")))) "iff" (Bool  "for" (Set (Var "i")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "I")) "holds"  (Bool   ($#r2_yellow_0 :::"ex_inf_of"::: )  (Set   ($#k5_waybel_3 :::"pi"::: )   "(" (Set (Var "X")) "," (Set (Var "i")) ")" ) "," (Set (Set (Var "J"))  ($#k2_yellow16 :::"."::: )  (Set (Var "i")))))  ")" )))) ; 
 
theorem :: YELLOW16:33 (Bool  "for" (Set (Var "I")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "J")) "being"   ($#v4_waybel_3 :::"non-Empty"::: )     ($#v1_yellow16 :::"Poset-yielding"::: )    ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I"))  (Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k5_yellow_1 :::"product"::: )  (Set (Var "J")) ")" )  "st" (Bool (Bool   ($#r1_yellow_0 :::"ex_sup_of"::: )  (Set (Var "X")) "," (Set   ($#k5_yellow_1 :::"product"::: )  (Set (Var "J"))))) "holds"  (Bool  "for" (Set (Var "i")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "I")) "holds"  (Bool (Set (Set  "("  ($#k1_yellow_0 :::"sup"::: )  (Set (Var "X")) ")" )  ($#k4_waybel_3 :::"."::: )  (Set (Var "i")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_yellow_0 :::"sup"::: )  (Set  "("  ($#k5_waybel_3 :::"pi"::: )   "(" (Set (Var "X")) "," (Set (Var "i")) ")"  ")" ))))))) ; 
 
theorem :: YELLOW16:34 (Bool  "for" (Set (Var "I")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "J")) "being"   ($#v4_waybel_3 :::"non-Empty"::: )     ($#v1_yellow16 :::"Poset-yielding"::: )    ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I"))  (Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k5_yellow_1 :::"product"::: )  (Set (Var "J")) ")" )  "st" (Bool (Bool   ($#r2_yellow_0 :::"ex_inf_of"::: )  (Set (Var "X")) "," (Set   ($#k5_yellow_1 :::"product"::: )  (Set (Var "J"))))) "holds"  (Bool  "for" (Set (Var "i")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "I")) "holds"  (Bool (Set (Set  "("  ($#k2_yellow_0 :::"inf"::: )  (Set (Var "X")) ")" )  ($#k4_waybel_3 :::"."::: )  (Set (Var "i")))  ($#r1_hidden :::"="::: )  (Set   ($#k2_yellow_0 :::"inf"::: )  (Set  "("  ($#k5_waybel_3 :::"pi"::: )   "(" (Set (Var "X")) "," (Set (Var "i")) ")"  ")" ))))))) ; 
 
theorem :: YELLOW16:35 (Bool  "for" (Set (Var "I")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "J")) "being"   ($#v1_yellow_1 :::"RelStr-yielding"::: )     ($#v4_waybel_3 :::"non-Empty"::: )     ($#v5_waybel_3 :::"reflexive-yielding"::: )    ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I"))  (Bool  "for" (Set (Var "X")) "being"   ($#v1_waybel_0 :::"directed"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k5_yellow_1 :::"product"::: )  (Set (Var "J")) ")" )  (Bool  "for" (Set (Var "i")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "I")) "holds"  (Bool (Set   ($#k5_waybel_3 :::"pi"::: )   "(" (Set (Var "X")) "," (Set (Var "i")) ")" ) "is"   ($#v1_waybel_0 :::"directed"::: )  ))))) ; 
 
theorem :: YELLOW16:36 (Bool  "for" (Set (Var "I")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "J")) "," (Set (Var "K")) "being"   ($#v1_yellow_1 :::"RelStr-yielding"::: )     ($#v4_waybel_3 :::"non-Empty"::: )    ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I"))  "st" (Bool (Bool  "("   "for" (Set (Var "i")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "I")) "holds"  (Bool (Set (Set (Var "K"))  ($#k3_waybel_3 :::"."::: )  (Set (Var "i"))) "is"    ($#m1_yellow_0 :::"SubRelStr"::: )   "of" (Set (Set (Var "J"))  ($#k3_waybel_3 :::"."::: )  (Set (Var "i"))))  ")" )) "holds"  (Bool (Set   ($#k5_yellow_1 :::"product"::: )  (Set (Var "K"))) "is"    ($#m1_yellow_0 :::"SubRelStr"::: )   "of" (Set   ($#k5_yellow_1 :::"product"::: )  (Set (Var "J")))))) ; 
 
theorem :: YELLOW16:37 (Bool  "for" (Set (Var "I")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "J")) "," (Set (Var "K")) "being"   ($#v1_yellow_1 :::"RelStr-yielding"::: )     ($#v4_waybel_3 :::"non-Empty"::: )    ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I"))  "st" (Bool (Bool  "("   "for" (Set (Var "i")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "I")) "holds"  (Bool (Set (Set (Var "K"))  ($#k3_waybel_3 :::"."::: )  (Set (Var "i"))) "is"   ($#v4_yellow_0 :::"full"::: )     ($#m1_yellow_0 :::"SubRelStr"::: )   "of" (Set (Set (Var "J"))  ($#k3_waybel_3 :::"."::: )  (Set (Var "i"))))  ")" )) "holds"  (Bool (Set   ($#k5_yellow_1 :::"product"::: )  (Set (Var "K"))) "is"   ($#v4_yellow_0 :::"full"::: )     ($#m1_yellow_0 :::"SubRelStr"::: )   "of" (Set   ($#k5_yellow_1 :::"product"::: )  (Set (Var "J")))))) ; 
 
theorem :: YELLOW16:38 (Bool  "for" (Set (Var "L")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "S")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#m1_yellow_0 :::"SubRelStr"::: )   "of" (Set (Var "L"))  (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set (Set (Var "S"))  ($#k6_yellow_1 :::"|^"::: )  (Set (Var "X"))) "is"    ($#m1_yellow_0 :::"SubRelStr"::: )   "of" (Set (Set (Var "L"))  ($#k6_yellow_1 :::"|^"::: )  (Set (Var "X"))))))) ; 
 
theorem :: YELLOW16:39 (Bool  "for" (Set (Var "L")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "S")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v4_yellow_0 :::"full"::: )     ($#m1_yellow_0 :::"SubRelStr"::: )   "of" (Set (Var "L"))  (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set (Set (Var "S"))  ($#k6_yellow_1 :::"|^"::: )  (Set (Var "X"))) "is"   ($#v4_yellow_0 :::"full"::: )     ($#m1_yellow_0 :::"SubRelStr"::: )   "of" (Set (Set (Var "L"))  ($#k6_yellow_1 :::"|^"::: )  (Set (Var "X"))))))) ; 
 begin  definitionlet "S", "T" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_orders_2 :::"RelStr"::: )  ; let "X" be    ($#m1_hidden :::"set"::: )  ; pred "S" :::"inherits_sup_of"::: "X" "," "T" means :: YELLOW16:def 6  "("  (Bool (Bool   ($#r1_yellow_0 :::"ex_sup_of"::: )  "X" "," "T")) "implies" (Bool (Set   ($#k1_yellow_0 :::""\/""::: )   "(" "X" "," "T" ")" )  ($#r2_hidden :::"in"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "S"))  ")" ; pred "S" :::"inherits_inf_of"::: "X" "," "T" means :: YELLOW16:def 7  "("  (Bool (Bool   ($#r2_yellow_0 :::"ex_inf_of"::: )  "X" "," "T")) "implies" (Bool (Set   ($#k2_yellow_0 :::""/\""::: )   "(" "X" "," "T" ")" )  ($#r2_hidden :::"in"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "S"))  ")" ; end; 












:: deftheorem    defines :::"inherits_sup_of"::: YELLOW16:def 6 :  (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 "X")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "S"))  ($#r5_yellow16 :::"inherits_sup_of"::: )  (Set (Var "X")) "," (Set (Var "T"))) "iff"  "("  (Bool (Bool   ($#r1_yellow_0 :::"ex_sup_of"::: )  (Set (Var "X")) "," (Set (Var "T")))) "implies" (Bool (Set   ($#k1_yellow_0 :::""\/""::: )   "(" (Set (Var "X")) "," (Set (Var "T")) ")" )  ($#r2_hidden :::"in"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "S"))))  ")"   ")" ))); 
 
:: deftheorem    defines :::"inherits_inf_of"::: YELLOW16:def 7 :  (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 "X")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "S"))  ($#r6_yellow16 :::"inherits_inf_of"::: )  (Set (Var "X")) "," (Set (Var "T"))) "iff"  "("  (Bool (Bool   ($#r2_yellow_0 :::"ex_inf_of"::: )  (Set (Var "X")) "," (Set (Var "T")))) "implies" (Bool (Set   ($#k2_yellow_0 :::""/\""::: )   "(" (Set (Var "X")) "," (Set (Var "T")) ")" )  ($#r2_hidden :::"in"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "S"))))  ")"   ")" ))); 
 
theorem :: YELLOW16:40 (Bool  "for" (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v4_orders_2 :::"transitive"::: )     ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "S")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v4_yellow_0 :::"full"::: )     ($#m1_yellow_0 :::"SubRelStr"::: )   "of" (Set (Var "T"))  (Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "S")) "holds"   (Bool  "("  (Bool (Set (Var "S"))  ($#r5_yellow16 :::"inherits_sup_of"::: )  (Set (Var "X")) "," (Set (Var "T"))) "iff"  "("  (Bool (Bool   ($#r1_yellow_0 :::"ex_sup_of"::: )  (Set (Var "X")) "," (Set (Var "T")))) "implies" (Bool  "("  (Bool   ($#r1_yellow_0 :::"ex_sup_of"::: )  (Set (Var "X")) "," (Set (Var "S"))) & (Bool (Set   ($#k1_yellow_0 :::"sup"::: )  (Set (Var "X")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_yellow_0 :::""\/""::: )   "(" (Set (Var "X")) "," (Set (Var "T")) ")" ))  ")" )  ")"   ")" )))) ; 
 
theorem :: YELLOW16:41 (Bool  "for" (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v4_orders_2 :::"transitive"::: )     ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "S")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v4_yellow_0 :::"full"::: )     ($#m1_yellow_0 :::"SubRelStr"::: )   "of" (Set (Var "T"))  (Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "S")) "holds"   (Bool  "("  (Bool (Set (Var "S"))  ($#r6_yellow16 :::"inherits_inf_of"::: )  (Set (Var "X")) "," (Set (Var "T"))) "iff"  "("  (Bool (Bool   ($#r2_yellow_0 :::"ex_inf_of"::: )  (Set (Var "X")) "," (Set (Var "T")))) "implies" (Bool  "("  (Bool   ($#r2_yellow_0 :::"ex_inf_of"::: )  (Set (Var "X")) "," (Set (Var "S"))) & (Bool (Set   ($#k2_yellow_0 :::"inf"::: )  (Set (Var "X")))  ($#r1_hidden :::"="::: )  (Set   ($#k2_yellow_0 :::""/\""::: )   "(" (Set (Var "X")) "," (Set (Var "T")) ")" ))  ")" )  ")"   ")" )))) ; 
 scheme  :: YELLOW16:sch 1 ProductSupsInheriting{ F1() ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  , F2() ->   ($#v4_waybel_3 :::"non-Empty"::: )     ($#v1_yellow16 :::"Poset-yielding"::: )    ($#m1_hidden :::"ManySortedSet":::) "of" (Set F1 "("  ")" ), F3() ->   ($#v4_waybel_3 :::"non-Empty"::: )     ($#v1_yellow16 :::"Poset-yielding"::: )    ($#m1_hidden :::"ManySortedSet":::) "of" (Set F1 "("  ")" ), P1[   ($#m1_hidden :::"set"::: )   ","    ($#m1_hidden :::"set"::: )  ] } : 
(Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k5_yellow_1 :::"product"::: )  (Set F3 "("  ")" ) ")" )  "st" (Bool (Bool P1[(Set (Var "X")) "," (Set   ($#k5_yellow_1 :::"product"::: )  (Set F3 "("  ")" ))])) "holds"  (Bool (Set   ($#k5_yellow_1 :::"product"::: )  (Set F3 "("  ")" ))  ($#r5_yellow16 :::"inherits_sup_of"::: )  (Set (Var "X")) "," (Set   ($#k5_yellow_1 :::"product"::: )  (Set F2 "("  ")" ))))
 provided
(Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k5_yellow_1 :::"product"::: )  (Set F3 "("  ")" ) ")" )  "st" (Bool (Bool P1[(Set (Var "X")) "," (Set   ($#k5_yellow_1 :::"product"::: )  (Set F3 "("  ")" ))])) "holds"  (Bool  "for" (Set (Var "i")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set F1 "("  ")" ) "holds"  (Bool P1[(Set   ($#k5_waybel_3 :::"pi"::: )   "(" (Set (Var "X")) "," (Set (Var "i")) ")" ) "," (Set (Set F3 "("  ")" )  ($#k2_yellow16 :::"."::: )  (Set (Var "i")))])))
 and  
(Bool  "for" (Set (Var "i")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set F1 "("  ")" ) "holds"  (Bool (Set (Set F3 "("  ")" )  ($#k2_yellow16 :::"."::: )  (Set (Var "i"))) "is"   ($#v4_yellow_0 :::"full"::: )     ($#m1_yellow_0 :::"SubRelStr"::: )   "of" (Set (Set F2 "("  ")" )  ($#k2_yellow16 :::"."::: )  (Set (Var "i")))))
 and  
(Bool  "for" (Set (Var "i")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set F1 "("  ")" )  (Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "(" (Set F3 "("  ")" )  ($#k2_yellow16 :::"."::: )  (Set (Var "i")) ")" )  "st" (Bool (Bool P1[(Set (Var "X")) "," (Set (Set F3 "("  ")" )  ($#k2_yellow16 :::"."::: )  (Set (Var "i")))])) "holds"  (Bool (Set (Set F3 "("  ")" )  ($#k2_yellow16 :::"."::: )  (Set (Var "i")))  ($#r5_yellow16 :::"inherits_sup_of"::: )  (Set (Var "X")) "," (Set (Set F2 "("  ")" )  ($#k2_yellow16 :::"."::: )  (Set (Var "i"))))))
 proof 


end; scheme  :: YELLOW16:sch 2 PowerSupsInheriting{ F1() ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  , F2() ->  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_orders_2 :::"Poset":::), F3() ->  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v4_yellow_0 :::"full"::: )     ($#m1_yellow_0 :::"SubRelStr"::: )   "of" (Set F2 "("  ")" ), P1[   ($#m1_hidden :::"set"::: )   ","    ($#m1_hidden :::"set"::: )  ] } : 
(Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "(" (Set F3 "("  ")" )  ($#k6_yellow_1 :::"|^"::: )  (Set F1 "("  ")" ) ")" )  "st" (Bool (Bool P1[(Set (Var "X")) "," (Set (Set F3 "("  ")" )  ($#k6_yellow_1 :::"|^"::: )  (Set F1 "("  ")" ))])) "holds"  (Bool (Set (Set F3 "("  ")" )  ($#k6_yellow_1 :::"|^"::: )  (Set F1 "("  ")" ))  ($#r5_yellow16 :::"inherits_sup_of"::: )  (Set (Var "X")) "," (Set (Set F2 "("  ")" )  ($#k6_yellow_1 :::"|^"::: )  (Set F1 "("  ")" ))))
 provided
(Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "(" (Set F3 "("  ")" )  ($#k6_yellow_1 :::"|^"::: )  (Set F1 "("  ")" ) ")" )  "st" (Bool (Bool P1[(Set (Var "X")) "," (Set (Set F3 "("  ")" )  ($#k6_yellow_1 :::"|^"::: )  (Set F1 "("  ")" ))])) "holds"  (Bool  "for" (Set (Var "i")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set F1 "("  ")" ) "holds"  (Bool P1[(Set   ($#k1_yellow16 :::"pi"::: )   "(" (Set (Var "X")) "," (Set (Var "i")) ")" ) "," (Set F3 "("  ")" )])))
 and  
(Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set F3 "("  ")" )  "st" (Bool (Bool P1[(Set (Var "X")) "," (Set F3 "("  ")" )])) "holds"  (Bool (Set F3 "("  ")" )  ($#r5_yellow16 :::"inherits_sup_of"::: )  (Set (Var "X")) "," (Set F2 "("  ")" )))
 proof 


end; scheme  :: YELLOW16:sch 3 ProductInfsInheriting{ F1() ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  , F2() ->   ($#v4_waybel_3 :::"non-Empty"::: )     ($#v1_yellow16 :::"Poset-yielding"::: )    ($#m1_hidden :::"ManySortedSet":::) "of" (Set F1 "("  ")" ), F3() ->   ($#v4_waybel_3 :::"non-Empty"::: )     ($#v1_yellow16 :::"Poset-yielding"::: )    ($#m1_hidden :::"ManySortedSet":::) "of" (Set F1 "("  ")" ), P1[   ($#m1_hidden :::"set"::: )   ","    ($#m1_hidden :::"set"::: )  ] } : 
(Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k5_yellow_1 :::"product"::: )  (Set F3 "("  ")" ) ")" )  "st" (Bool (Bool P1[(Set (Var "X")) "," (Set   ($#k5_yellow_1 :::"product"::: )  (Set F3 "("  ")" ))])) "holds"  (Bool (Set   ($#k5_yellow_1 :::"product"::: )  (Set F3 "("  ")" ))  ($#r6_yellow16 :::"inherits_inf_of"::: )  (Set (Var "X")) "," (Set   ($#k5_yellow_1 :::"product"::: )  (Set F2 "("  ")" ))))
 provided
(Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k5_yellow_1 :::"product"::: )  (Set F3 "("  ")" ) ")" )  "st" (Bool (Bool P1[(Set (Var "X")) "," (Set   ($#k5_yellow_1 :::"product"::: )  (Set F3 "("  ")" ))])) "holds"  (Bool  "for" (Set (Var "i")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set F1 "("  ")" ) "holds"  (Bool P1[(Set   ($#k5_waybel_3 :::"pi"::: )   "(" (Set (Var "X")) "," (Set (Var "i")) ")" ) "," (Set (Set F3 "("  ")" )  ($#k2_yellow16 :::"."::: )  (Set (Var "i")))])))
 and  
(Bool  "for" (Set (Var "i")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set F1 "("  ")" ) "holds"  (Bool (Set (Set F3 "("  ")" )  ($#k2_yellow16 :::"."::: )  (Set (Var "i"))) "is"   ($#v4_yellow_0 :::"full"::: )     ($#m1_yellow_0 :::"SubRelStr"::: )   "of" (Set (Set F2 "("  ")" )  ($#k2_yellow16 :::"."::: )  (Set (Var "i")))))
 and  
(Bool  "for" (Set (Var "i")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set F1 "("  ")" )  (Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "(" (Set F3 "("  ")" )  ($#k2_yellow16 :::"."::: )  (Set (Var "i")) ")" )  "st" (Bool (Bool P1[(Set (Var "X")) "," (Set (Set F3 "("  ")" )  ($#k2_yellow16 :::"."::: )  (Set (Var "i")))])) "holds"  (Bool (Set (Set F3 "("  ")" )  ($#k2_yellow16 :::"."::: )  (Set (Var "i")))  ($#r6_yellow16 :::"inherits_inf_of"::: )  (Set (Var "X")) "," (Set (Set F2 "("  ")" )  ($#k2_yellow16 :::"."::: )  (Set (Var "i"))))))
 proof 


end; scheme  :: YELLOW16:sch 4 PowerInfsInheriting{ F1() ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  , F2() ->  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_orders_2 :::"Poset":::), F3() ->  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v4_yellow_0 :::"full"::: )     ($#m1_yellow_0 :::"SubRelStr"::: )   "of" (Set F2 "("  ")" ), P1[   ($#m1_hidden :::"set"::: )   ","    ($#m1_hidden :::"set"::: )  ] } : 
(Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "(" (Set F3 "("  ")" )  ($#k6_yellow_1 :::"|^"::: )  (Set F1 "("  ")" ) ")" )  "st" (Bool (Bool P1[(Set (Var "X")) "," (Set (Set F3 "("  ")" )  ($#k6_yellow_1 :::"|^"::: )  (Set F1 "("  ")" ))])) "holds"  (Bool (Set (Set F3 "("  ")" )  ($#k6_yellow_1 :::"|^"::: )  (Set F1 "("  ")" ))  ($#r6_yellow16 :::"inherits_inf_of"::: )  (Set (Var "X")) "," (Set (Set F2 "("  ")" )  ($#k6_yellow_1 :::"|^"::: )  (Set F1 "("  ")" ))))
 provided
(Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "(" (Set F3 "("  ")" )  ($#k6_yellow_1 :::"|^"::: )  (Set F1 "("  ")" ) ")" )  "st" (Bool (Bool P1[(Set (Var "X")) "," (Set (Set F3 "("  ")" )  ($#k6_yellow_1 :::"|^"::: )  (Set F1 "("  ")" ))])) "holds"  (Bool  "for" (Set (Var "i")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set F1 "("  ")" ) "holds"  (Bool P1[(Set   ($#k1_yellow16 :::"pi"::: )   "(" (Set (Var "X")) "," (Set (Var "i")) ")" ) "," (Set F3 "("  ")" )])))
 and  
(Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set F3 "("  ")" )  "st" (Bool (Bool P1[(Set (Var "X")) "," (Set F3 "("  ")" )])) "holds"  (Bool (Set F3 "("  ")" )  ($#r6_yellow16 :::"inherits_inf_of"::: )  (Set (Var "X")) "," (Set F2 "("  ")" )))
 proof 


end; registrationlet "I" be    ($#m1_hidden :::"set"::: )  ; let "L" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_orders_2 :::"RelStr"::: )  ; let "X" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_subset_1 :::"Subset":::) "of" (Set  "(" (Set (Const "L"))  ($#k6_yellow_1 :::"|^"::: )  (Set (Const "I")) ")" ); let "i" be    ($#m1_hidden :::"set"::: )  ; 
cluster (Set   ($#k5_card_3 :::"pi"::: )   "(" "X" "," "i" ")" ) ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )  ; 
end; 
theorem :: YELLOW16:42 (Bool  "for" (Set (Var "L")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_orders_2 :::"Poset":::)  (Bool  "for" (Set (Var "S")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v4_yellow_0 :::"full"::: )     ($#v4_waybel_0 :::"directed-sups-inheriting"::: )     ($#m1_yellow_0 :::"SubRelStr"::: )   "of" (Set (Var "L"))  (Bool  "for" (Set (Var "X")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set (Set (Var "S"))  ($#k6_yellow_1 :::"|^"::: )  (Set (Var "X"))) "is"   ($#v4_waybel_0 :::"directed-sups-inheriting"::: )     ($#m1_yellow_0 :::"SubRelStr"::: )   "of" (Set (Set (Var "L"))  ($#k6_yellow_1 :::"|^"::: )  (Set (Var "X"))))))) ; 
 registrationlet "I" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  ; let "J" be   ($#v1_yellow_1 :::"RelStr-yielding"::: )     ($#v4_waybel_3 :::"non-Empty"::: )    ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I")); let "X" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k5_yellow_1 :::"product"::: )  (Set (Const "J")) ")" ); let "i" be    ($#m1_hidden :::"set"::: )  ; 
cluster (Set   ($#k5_card_3 :::"pi"::: )   "(" "X" "," "i" ")" ) ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )  ; 
end; 
theorem :: YELLOW16:43 (Bool  "for" (Set (Var "X")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "L")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v24_waybel_0 :::"up-complete"::: )    ($#l1_orders_2 :::"Poset":::) "holds"  (Bool (Set (Set (Var "L"))  ($#k6_yellow_1 :::"|^"::: )  (Set (Var "X"))) "is"   ($#v24_waybel_0 :::"up-complete"::: )  ))) ; 
 registrationlet "L" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v24_waybel_0 :::"up-complete"::: )    ($#l1_orders_2 :::"Poset":::); let "X" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  ; 
cluster (Set "L"  ($#k6_yellow_1 :::"|^"::: )  "X") ->   ($#v24_waybel_0 :::"up-complete"::: )   ; 
end; begin  
theorem :: YELLOW16:44 (Bool  "for" (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "S")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#m1_pre_topc :::"SubSpace"::: )   "of" (Set (Var "T"))  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "T")) "," (Set (Var "S"))  "st" (Bool (Bool (Set (Var "f")) "is"   ($#v3_borsuk_1 :::"being_a_retraction"::: )  )) "holds"  (Bool (Set   ($#k2_relset_1 :::"rng"::: )  (Set (Var "f")))  ($#r1_hidden :::"="::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "S"))))))) ; 
 
theorem :: YELLOW16:45 (Bool  "for" (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "S")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#m1_pre_topc :::"SubSpace"::: )   "of" (Set (Var "T"))  (Bool  "for" (Set (Var "f")) "being"   ($#v5_pre_topc :::"continuous"::: )    ($#m1_subset_1 :::"Function":::) "of" (Set (Var "T")) "," (Set (Var "S"))  "st" (Bool (Bool (Set (Var "f")) "is"   ($#v3_borsuk_1 :::"being_a_retraction"::: )  )) "holds"  (Bool (Set (Var "f")) "is"   ($#v11_quantal1 :::"idempotent"::: )  )))) ; 
 
theorem :: YELLOW16:46 (Bool  "for" (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "V")) "being"   ($#v3_pre_topc :::"open"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "holds"  (Bool (Set   ($#k5_funct_3 :::"chi"::: )   "(" (Set (Var "V")) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "T"))) ")" ) "is"   ($#v5_pre_topc :::"continuous"::: )    ($#m1_subset_1 :::"Function":::) "of" (Set (Var "T")) "," (Set  ($#k9_waybel18 :::"Sierpinski_Space"::: ) )))) ; 
 
theorem :: YELLOW16:47 (Bool  "for" (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "T"))  "st" (Bool (Bool  "("   "for" (Set (Var "W")) "being"   ($#v3_pre_topc :::"open"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T"))  "st" (Bool (Bool (Set (Var "y"))  ($#r2_hidden :::"in"::: )  (Set (Var "W")))) "holds"  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "W")))  ")" )) "holds"  (Bool (Set  "(" (Set  ($#k6_numbers :::"0"::: ) ) "," (Num 1) ")"   ($#k5_funct_4 :::"-->"::: )   "(" (Set (Var "y")) "," (Set (Var "x")) ")" ) "is"   ($#v5_pre_topc :::"continuous"::: )    ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k9_waybel18 :::"Sierpinski_Space"::: ) ) "," (Set (Var "T"))))) ; 
 
theorem :: YELLOW16:48 (Bool  "for" (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "T"))  (Bool  "for" (Set (Var "V")) "being"   ($#v3_pre_topc :::"open"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T"))  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "V"))) & (Bool (Bool  "not" (Set (Var "y"))  ($#r2_hidden :::"in"::: )  (Set (Var "V"))))) "holds"  (Bool (Set (Set  "("  ($#k5_funct_3 :::"chi"::: )   "(" (Set (Var "V")) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "T"))) ")"  ")" )  ($#k1_partfun1 :::"*"::: )  (Set  "("  "(" (Set  ($#k6_numbers :::"0"::: ) ) "," (Num 1) ")"   ($#k5_funct_4 :::"-->"::: )   "(" (Set (Var "y")) "," (Set (Var "x")) ")"  ")" ))  ($#r1_funct_2 :::"="::: )  (Set   ($#k3_struct_0 :::"id"::: )  (Set  ($#k9_waybel18 :::"Sierpinski_Space"::: ) )))))) ; 
 
theorem :: YELLOW16:49 (Bool  "for" (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_struct_0 :::"1-sorted"::: )    (Bool  "for" (Set (Var "V")) "," (Set (Var "W")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T"))  (Bool  "for" (Set (Var "S")) "being"    ($#m1_yellow_9 :::"TopAugmentation"::: )   "of" (Set   ($#k3_yellow_1 :::"BoolePoset"::: )  (Num 1))  (Bool  "for" (Set (Var "f")) "," (Set (Var "g")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "T")) "," (Set (Var "S"))  "st" (Bool (Bool (Set (Var "f"))  ($#r1_hidden :::"="::: )  (Set   ($#k5_funct_3 :::"chi"::: )   "(" (Set (Var "V")) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "T"))) ")" )) & (Bool (Set (Var "g"))  ($#r1_hidden :::"="::: )  (Set   ($#k5_funct_3 :::"chi"::: )   "(" (Set (Var "W")) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "T"))) ")" ))) "holds"  (Bool  "("  (Bool (Set (Var "V"))  ($#r1_tarski :::"c="::: )  (Set (Var "W"))) "iff" (Bool (Set (Var "f"))  ($#r1_yellow_2 :::"<="::: )  (Set (Var "g")))  ")" ))))) ; 
 
theorem :: YELLOW16:50 (Bool  "for" (Set (Var "L")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "X")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "R")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v4_yellow_0 :::"full"::: )     ($#m1_yellow_0 :::"SubRelStr"::: )   "of" (Set (Set (Var "L"))  ($#k6_yellow_1 :::"|^"::: )  (Set (Var "X")))  "st" (Bool (Bool  "("   "for" (Set (Var "a")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "a")) "is"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R"))) "iff" (Bool  "ex" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "X"))  ($#k8_funcop_1 :::"-->"::: )  (Set (Var "x")))))  ")" )  ")" )) "holds"  (Bool (Set (Var "L")) "," (Set (Var "R"))  ($#r5_waybel_1 :::"are_isomorphic"::: )  )))) ; 
 
theorem :: YELLOW16:51 (Bool  "for" (Set (Var "S")) "," (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::) "holds"   (Bool  "("  (Bool (Set (Var "S")) "," (Set (Var "T"))  ($#r1_t_0topsp :::"are_homeomorphic"::: )  ) "iff" (Bool  "ex" (Set (Var "f")) "being"   ($#v5_pre_topc :::"continuous"::: )    ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set (Var "T"))(Bool  "ex" (Set (Var "g")) "being"   ($#v5_pre_topc :::"continuous"::: )    ($#m1_subset_1 :::"Function":::) "of" (Set (Var "T")) "," (Set (Var "S")) "st"  (Bool  "("  (Bool (Set (Set (Var "f"))  ($#k1_partfun1 :::"*"::: )  (Set (Var "g")))  ($#r2_funct_2 :::"="::: )  (Set   ($#k3_struct_0 :::"id"::: )  (Set (Var "T")))) & (Bool (Set (Set (Var "g"))  ($#k1_partfun1 :::"*"::: )  (Set (Var "f")))  ($#r2_funct_2 :::"="::: )  (Set   ($#k3_struct_0 :::"id"::: )  (Set (Var "S"))))  ")" )))  ")" )) ; 
 
theorem :: YELLOW16:52 (Bool  "for" (Set (Var "T")) "," (Set (Var "S")) "," (Set (Var "R")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "T")) "," (Set (Var "S"))  (Bool  "for" (Set (Var "g")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set (Var "T"))  (Bool  "for" (Set (Var "h")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set (Var "R"))  "st" (Bool (Bool (Set (Set (Var "f"))  ($#k1_partfun1 :::"*"::: )  (Set (Var "g")))  ($#r2_funct_2 :::"="::: )  (Set   ($#k3_struct_0 :::"id"::: )  (Set (Var "S")))) & (Bool (Set (Var "h")) "is"   ($#v3_tops_2 :::"being_homeomorphism"::: )  )) "holds"  (Bool (Set (Set  "(" (Set (Var "h"))  ($#k1_partfun1 :::"*"::: )  (Set (Var "f")) ")" )  ($#k1_partfun1 :::"*"::: )  (Set  "(" (Set (Var "g"))  ($#k1_partfun1 :::"*"::: )  (Set  "(" (Set (Var "h"))  ($#k2_tops_2 :::"""::: )  ")" ) ")" ))  ($#r2_funct_2 :::"="::: )  (Set   ($#k3_struct_0 :::"id"::: )  (Set (Var "R")))))))) ; 
 
theorem :: YELLOW16:53 (Bool  "for" (Set (Var "T")) "," (Set (Var "S")) "," (Set (Var "R")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::)  "st" (Bool (Bool (Set (Var "S"))  ($#r1_waybel18 :::"is_Retract_of"::: )  (Set (Var "T"))) & (Bool (Set (Var "S")) "," (Set (Var "R"))  ($#r1_t_0topsp :::"are_homeomorphic"::: )  )) "holds"  (Bool (Set (Var "R"))  ($#r1_waybel18 :::"is_Retract_of"::: )  (Set (Var "T")))) ; 
 
theorem :: YELLOW16:54 (Bool  "for" (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "S")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#m1_pre_topc :::"SubSpace"::: )   "of" (Set (Var "T")) "holds"  (Bool (Set   ($#k1_yellow_9 :::"incl"::: )   "(" (Set (Var "S")) "," (Set (Var "T")) ")" ) "is"   ($#v5_pre_topc :::"continuous"::: )  ))) ; 
 
theorem :: YELLOW16:55 (Bool  "for" (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "S")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#m1_pre_topc :::"SubSpace"::: )   "of" (Set (Var "T"))  (Bool  "for" (Set (Var "f")) "being"   ($#v5_pre_topc :::"continuous"::: )    ($#m1_subset_1 :::"Function":::) "of" (Set (Var "T")) "," (Set (Var "S"))  "st" (Bool (Bool (Set (Var "f")) "is"   ($#v3_borsuk_1 :::"being_a_retraction"::: )  )) "holds"  (Bool (Set (Set (Var "f"))  ($#k1_partfun1 :::"*"::: )  (Set  "("  ($#k1_yellow_9 :::"incl"::: )   "(" (Set (Var "S")) "," (Set (Var "T")) ")"  ")" ))  ($#r2_funct_2 :::"="::: )  (Set   ($#k3_struct_0 :::"id"::: )  (Set (Var "S"))))))) ; 
 
theorem :: YELLOW16:56 (Bool  "for" (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "S")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#m1_pre_topc :::"SubSpace"::: )   "of" (Set (Var "T"))  "st" (Bool (Bool (Set (Var "S"))  ($#r1_borsuk_1 :::"is_a_retract_of"::: )  (Set (Var "T")))) "holds"  (Bool (Set (Var "S"))  ($#r1_waybel18 :::"is_Retract_of"::: )  (Set (Var "T"))))) ; 
 
theorem :: YELLOW16:57 (Bool  "for" (Set (Var "R")) "," (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::) "holds"   (Bool  "("  (Bool (Set (Var "R"))  ($#r1_waybel18 :::"is_Retract_of"::: )  (Set (Var "T"))) "iff" (Bool  "ex" (Set (Var "S")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#m1_pre_topc :::"SubSpace"::: )   "of" (Set (Var "T")) "st"  (Bool  "("  (Bool (Set (Var "S"))  ($#r1_borsuk_1 :::"is_a_retract_of"::: )  (Set (Var "T"))) & (Bool (Set (Var "S")) "," (Set (Var "R"))  ($#r1_t_0topsp :::"are_homeomorphic"::: )  )  ")" ))  ")" )) ;