:: YELLOW16 semantic presentation

theorem Th1: :: YELLOW16:1

for b₁, b₂ being Relation holds b₁ * b₂ = b₁ (#) b₂

proof end;

theorem Th2: :: YELLOW16:2

for b₁ being set
for b₂ being non empty RelStr
for b₃ being non empty SubRelStr of b₂
for b₄, b₅ being Function of b₁,the carrier of b₃
for b₆, b₇ being Function of b₁,the carrier of b₂ st b₆ = b₄ & b₇ = b₅ & b₄ <= b₅ holds
b₆ <= b₇

proof end;

theorem Th3: :: YELLOW16:3

for b₁ being set
for b₂ being non empty RelStr
for b₃ being non empty full SubRelStr of b₂
for b₄, b₅ being Function of b₁,the carrier of b₃
for b₆, b₇ being Function of b₁,the carrier of b₂ st b₆ = b₄ & b₇ = b₅ & b₆ <= b₇ holds
b₄ <= b₅

proof end;

registration

let c₁ be non empty RelStr ;
let c₂ be non empty reflexive antisymmetric RelStr ;
cluster monotone directed-sups-preserving M5(the carrier of a₁,the carrier of a₂);
existence

proof end;

end;

theorem Th4: :: YELLOW16:4

for b₁, b₂ being Function st b₁ is idempotent & rng b₂ c= rng b₁ & rng b₂ c= dom b₁ holds
b₁ * b₂ = b₂

proof end;

registration

let c₁ be 1-sorted ;
cluster idempotent M5(the carrier of a₁,the carrier of a₁);
existence

proof end;

end;

theorem Th5: :: YELLOW16:5

for b₁ being non empty up-complete Poset
for b₂ being non empty full directed-sups-inheriting SubRelStr of b₁ holds b₂ is up-complete

proof end;

theorem Th6: :: YELLOW16:6

for b₁ being non empty up-complete Poset
for b₂ being Function of b₁,b₁ st b₂ is idempotent & b₂ is directed-sups-preserving holds
Image b₂ is directed-sups-inheriting

proof end;

theorem Th7: :: YELLOW16:7

canceled;

theorem Th8: :: YELLOW16:8

for b₁, b₂ being non empty 1-sorted
for b₃ being Function of b₂,b₁
for b₄ being Function of b₁,b₂ st b₃ * b₄ = id b₁ holds
rng b₃ = the carrier of b₁

proof end;

theorem Th9: :: YELLOW16:9

for b₁ being non empty RelStr
for b₂ being non empty SubRelStr of b₁
for b₃ being Function of b₁,b₂ st b₃ * (incl b₂,b₁) = id b₂ holds
b₃ is idempotent Function of b₁,b₁

proof end;

definition

let c₁, c₂ be non empty Poset;
let c₃ be Function;
pred c₃ is_a_retraction_of c₂,c₁ means :Def1: :: YELLOW16:def 1
( a₃ is directed-sups-preserving Function of a₂,a₁ & a₃ | the carrier of a₁ = id a₁ & a₁ is full directed-sups-inheriting SubRelStr of a₂ );
pred c₃ is_an_UPS_retraction_of c₂,c₁ means :Def2: :: YELLOW16:def 2
( a₃ is directed-sups-preserving Function of a₂,a₁ & ex b₁ being directed-sups-preserving Function of a₁,a₂ st a₃ * b₁ = id a₁ );

end;

:: deftheorem Def1 defines is_a_retraction_of YELLOW16:def 1 :

:: deftheorem Def2 defines is_an_UPS_retraction_of YELLOW16:def 2 :

definition

let c₁, c₂ be non empty Poset;
pred c₁ is_a_retract_of c₂ means :Def3: :: YELLOW16:def 3
ex b₁ being Function of a₂,a₁ st b₁ is_a_retraction_of a₂,a₁;
pred c₁ is_an_UPS_retract_of c₂ means :Def4: :: YELLOW16:def 4
ex b₁ being Function of a₂,a₁ st b₁ is_an_UPS_retraction_of a₂,a₁;

end;

:: deftheorem Def3 defines is_a_retract_of YELLOW16:def 3 :

:: deftheorem Def4 defines is_an_UPS_retract_of YELLOW16:def 4 :

theorem Th10: :: YELLOW16:10

for b₁, b₂ being non empty Poset
for b₃ being Function st b₃ is_a_retraction_of b₂,b₁ holds
b₃ * (incl b₁,b₂) = id b₁

proof end;

theorem Th11: :: YELLOW16:11

for b₁ being non empty Poset
for b₂ being non empty up-complete Poset
for b₃ being Function st b₃ is_a_retraction_of b₂,b₁ holds
b₃ is_an_UPS_retraction_of b₂,b₁

proof end;

theorem Th12: :: YELLOW16:12

for b₁, b₂ being non empty Poset
for b₃ being Function st b₃ is_a_retraction_of b₂,b₁ holds
rng b₃ = the carrier of b₁

proof end;

theorem Th13: :: YELLOW16:13

for b₁, b₂ being non empty Poset
for b₃ being Function st b₃ is_an_UPS_retraction_of b₂,b₁ holds
rng b₃ = the carrier of b₁

proof end;

theorem Th14: :: YELLOW16:14

for b₁, b₂ being non empty Poset
for b₃ being Function st b₃ is_a_retraction_of b₂,b₁ holds
b₃ is idempotent Function of b₂,b₂

proof end;

theorem Th15: :: YELLOW16:15

for b₁, b₂ being non empty Poset
for b₃ being Function of b₁,b₁ st b₃ is_a_retraction_of b₁,b₂ holds
Image b₃ = RelStr(# the carrier of b₂,the InternalRel of b₂ #)

proof end;

theorem Th16: :: YELLOW16:16

for b₁ being non empty up-complete Poset
for b₂ being non empty Poset
for b₃ being Function of b₁,b₁ st b₃ is_a_retraction_of b₁,b₂ holds
( b₃ is directed-sups-preserving & b₃ is projection )

proof end;

theorem Th17: :: YELLOW16:17

for b₁, b₂ being non empty reflexive transitive RelStr
for b₃ being Function of b₁,b₂ holds
( b₃ is isomorphic iff ( b₃ is monotone & ex b₄ being monotone Function of b₂,b₁ st
( b₃ * b₄ = id b₂ & b₄ * b₃ = id b₁ ) ) )

proof end;

theorem Th18: :: YELLOW16:18

for b₁, b₂ being non empty Poset holds
( b₁,b₂ are_isomorphic iff ex b₃ being monotone Function of b₁,b₂ex b₄ being monotone Function of b₂,b₁ st
( b₃ * b₄ = id b₂ & b₄ * b₃ = id b₁ ) )

proof end;

theorem Th19: :: YELLOW16:19

for b₁, b₂ being non empty up-complete Poset st b₁,b₂ are_isomorphic holds
( b₁ is_an_UPS_retract_of b₂ & b₂ is_an_UPS_retract_of b₁ )

proof end;

theorem Th20: :: YELLOW16:20

for b₁, b₂ being non empty Poset
for b₃ being monotone Function of b₁,b₂
for b₄ being monotone Function of b₂,b₁ st b₃ * b₄ = id b₂ holds
ex b₅ being projection Function of b₁,b₁ st
( b₅ = b₄ * b₃ & b₅ | the carrier of (Image b₅) = id (Image b₅) & b₂, Image b₅ are_isomorphic )

proof end;

theorem Th21: :: YELLOW16:21

for b₁ being non empty up-complete Poset
for b₂ being non empty Poset
for b₃ being Function st b₃ is_an_UPS_retraction_of b₁,b₂ holds
ex b₄ being directed-sups-preserving projection Function of b₁,b₁ st
( b₄ is_a_retraction_of b₁, Image b₄ & b₂, Image b₄ are_isomorphic )

proof end;

theorem Th22: :: YELLOW16:22

for b₁ being non empty up-complete Poset
for b₂ being non empty Poset st b₂ is_a_retract_of b₁ holds
b₂ is up-complete

proof end;

theorem Th23: :: YELLOW16:23

for b₁ being non empty complete Poset
for b₂ being non empty Poset st b₂ is_a_retract_of b₁ holds
b₂ is complete

proof end;

theorem Th24: :: YELLOW16:24

for b₁ being complete continuous LATTICE
for b₂ being non empty Poset st b₂ is_a_retract_of b₁ holds
b₂ is continuous

proof end;

theorem Th25: :: YELLOW16:25

for b₁ being non empty up-complete Poset
for b₂ being non empty Poset st b₂ is_an_UPS_retract_of b₁ holds
b₂ is up-complete

proof end;

theorem Th26: :: YELLOW16:26

for b₁ being non empty complete Poset
for b₂ being non empty Poset st b₂ is_an_UPS_retract_of b₁ holds
b₂ is complete

proof end;

theorem Th27: :: YELLOW16:27

for b₁ being complete continuous LATTICE
for b₂ being non empty Poset st b₂ is_an_UPS_retract_of b₁ holds
b₂ is continuous

proof end;

theorem Th28: :: YELLOW16:28

for b₁ being RelStr
for b₂ being full SubRelStr of b₁
for b₃ being SubRelStr of b₂ holds
( b₃ is full iff b₃ is full SubRelStr of b₁ )

proof end;

theorem Th29: :: YELLOW16:29

for b₁ being non empty transitive RelStr
for b₂ being non empty full directed-sups-inheriting SubRelStr of b₁
for b₃ being non empty directed-sups-inheriting SubRelStr of b₂ holds b₃ is directed-sups-inheriting SubRelStr of b₁

proof end;

theorem Th30: :: YELLOW16:30

for b₁ being non empty up-complete Poset
for b₂, b₃ being non empty full directed-sups-inheriting SubRelStr of b₁ st b₂ is SubRelStr of b₃ holds
b₂ is full directed-sups-inheriting SubRelStr of b₃

proof end;

definition

let c₁ be Relation;
attr a₁ is Poset-yielding means :Def5: :: YELLOW16:def 5
for b₁ being set st b₁ in rng a₁ holds
b₁ is Poset;

end;

:: deftheorem Def5 defines Poset-yielding YELLOW16:def 5 :

registration

cluster Poset-yielding -> RelStr-yielding reflexive-yielding set ;
coherence

proof end;

end;

definition

let c₁ be non empty set ;
let c₂ be non empty RelStr ;
let c₃ be Element of c₁;
let c₄ be Subset of (c₂ |^ c₁);
redefine func pi as pi c₄,c₃ -> Subset of a₂;
coherence

proof end;

end;

registration

let c₁ be set ;
let c₂ be Poset;
cluster K104(a₁,a₂) -> Poset-yielding ;
coherence

proof end;

end;

registration

let c₁ be set ;
cluster RelStr-yielding non-Empty reflexive-yielding Poset-yielding ManySortedSet of a₁;
existence

proof end;

end;

registration

let c₁ be non empty set ;
let c₂ be non-Empty Poset-yielding ManySortedSet of c₁;
cluster product a₂ -> transitive antisymmetric ;
coherence

proof end;

end;

definition

let c₁ be non empty set ;
let c₂ be non-Empty Poset-yielding ManySortedSet of c₁;
let c₃ be Element of c₁;
redefine func . as c₂ . c₃ -> non empty Poset;
coherence

proof end;

end;

E25: now

let c₁ be non empty set ;
let c₂ be non-Empty Poset-yielding ManySortedSet of c₁;
let c₃ be Subset of (product c₂);
deffunc H₁( Element of c₁) -> Element of the carrier of (c₂ . a₁) = sup (pi c₃,a₁);
consider c₄ being ManySortedSet of c₁ such that
E26: for b₁ being Element of c₁ holds c₄ . b₁ = H₁(b₁) from PBOOLE:sch 5();
E27: dom c₄ = c₁ by PBOOLE:def 3;

now

let c₅ be Element of c₁;
c₄ . c₅ = sup (pi c₃,c₅) by E26;
hence c₄ . c₅ is Element of (c₂ . c₅) ;

end;

then reconsider c₅ = c₄ as Element of (product c₂) by E27, WAYBEL_3:27;
assume E28: for b₁ being Element of c₁ holds ex_sup_of pi c₃,b₁,c₂ . b₁ ;
take c₆ = c₅;
thus for b₁ being Element of c₁ holds c₆ . b₁ = sup (pi c₃,b₁) by E26;
thus c₆ is_>=_than c₃

proof

let c₇ be Element of (product c₂); :: according to LATTICE3:def 9
assume E29: c₇ in c₃ ;

now

let c₈ be Element of c₁;
( ex_sup_of pi c₃,c₈,c₂ . c₈ & c₆ . c₈ = sup (pi c₃,c₈) ) by E26, E28;
then ( c₆ . c₈ is_>=_than pi c₃,c₈ & c₇ . c₈ in pi c₃,c₈ ) by E29, CARD_3:def 6, YELLOW_0:30;
hence c₇ . c₈ <= c₆ . c₈ by LATTICE3:def 9;

end;

hence c₇ <= c₆ by WAYBEL_3:28;

end;

let c₇ be Element of (product c₂);
assume E29: c₃ is_<=_than c₇ ;

now

let c₈ be Element of c₁;
E30: ( c₆ . c₈ = sup (pi c₃,c₈) & ex_sup_of pi c₃,c₈,c₂ . c₈ ) by E26, E28;
c₇ . c₈ is_>=_than pi c₃,c₈

proof

let c₉ be Element of (c₂ . c₈); :: according to LATTICE3:def 9
assume c₉ in pi c₃,c₈ ;
then consider c₁₀ being Function such that
E31: ( c₁₀ in c₃ & c₉ = c₁₀ . c₈ ) by CARD_3:def 6;
reconsider c₁₁ = c₁₀ as Element of (product c₂) by E31;
c₁₁ <= c₇ by E29, E31, LATTICE3:def 9;
hence c₉ <= c₇ . c₈ by E31, WAYBEL_3:28;

end;

hence c₆ . c₈ <= c₇ . c₈ by E30, YELLOW_0:30;

end;

hence c₆ <= c₇ by WAYBEL_3:28;

end;

E26: now

let c₁ be non empty set ;
let c₂ be non-Empty Poset-yielding ManySortedSet of c₁;
let c₃ be Subset of (product c₂);
deffunc H₁( Element of c₁) -> Element of the carrier of (c₂ . a₁) = inf (pi c₃,a₁);
consider c₄ being ManySortedSet of c₁ such that
E27: for b₁ being Element of c₁ holds c₄ . b₁ = H₁(b₁) from PBOOLE:sch 5();
E28: dom c₄ = c₁ by PBOOLE:def 3;

now

let c₅ be Element of c₁;
c₄ . c₅ = inf (pi c₃,c₅) by E27;
hence c₄ . c₅ is Element of (c₂ . c₅) ;

end;

then reconsider c₅ = c₄ as Element of (product c₂) by E28, WAYBEL_3:27;
assume E29: for b₁ being Element of c₁ holds ex_inf_of pi c₃,b₁,c₂ . b₁ ;
take c₆ = c₅;
thus for b₁ being Element of c₁ holds c₆ . b₁ = inf (pi c₃,b₁) by E27;
thus c₆ is_<=_than c₃

proof

let c₇ be Element of (product c₂); :: according to LATTICE3:def 8
assume E30: c₇ in c₃ ;

now

let c₈ be Element of c₁;
( ex_inf_of pi c₃,c₈,c₂ . c₈ & c₆ . c₈ = inf (pi c₃,c₈) ) by E27, E29;
then ( c₆ . c₈ is_<=_than pi c₃,c₈ & c₇ . c₈ in pi c₃,c₈ ) by E30, CARD_3:def 6, YELLOW_0:31;
hence c₇ . c₈ >= c₆ . c₈ by LATTICE3:def 8;

end;

hence c₆ <= c₇ by WAYBEL_3:28;

end;

let c₇ be Element of (product c₂);
assume E30: c₃ is_>=_than c₇ ;

now

let c₈ be Element of c₁;
E31: ( c₆ . c₈ = inf (pi c₃,c₈) & ex_inf_of pi c₃,c₈,c₂ . c₈ ) by E27, E29;
c₇ . c₈ is_<=_than pi c₃,c₈

proof

let c₉ be Element of (c₂ . c₈); :: according to LATTICE3:def 8
assume c₉ in pi c₃,c₈ ;
then consider c₁₀ being Function such that
E32: ( c₁₀ in c₃ & c₉ = c₁₀ . c₈ ) by CARD_3:def 6;
reconsider c₁₁ = c₁₀ as Element of (product c₂) by E32;
c₁₁ >= c₇ by E30, E32, LATTICE3:def 8;
hence c₉ >= c₇ . c₈ by E32, WAYBEL_3:28;

end;

hence c₆ . c₈ >= c₇ . c₈ by E31, YELLOW_0:31;

end;

hence c₆ >= c₇ by WAYBEL_3:28;

end;

theorem Th31: :: YELLOW16:31

for b₁ being non empty set
for b₂ being non-Empty Poset-yielding ManySortedSet of b₁
for b₃ being Element of (product b₂)
for b₄ being Subset of (product b₂) holds
( b₃ is_>=_than b₄ iff for b₅ being Element of b₁ holds b₃ . b₅ is_>=_than pi b₄,b₅ )

proof end;

theorem Th32: :: YELLOW16:32

for b₁ being non empty set
for b₂ being non-Empty Poset-yielding ManySortedSet of b₁
for b₃ being Element of (product b₂)
for b₄ being Subset of (product b₂) holds
( b₃ is_<=_than b₄ iff for b₅ being Element of b₁ holds b₃ . b₅ is_<=_than pi b₄,b₅ )

proof end;

theorem Th33: :: YELLOW16:33

for b₁ being non empty set
for b₂ being non-Empty Poset-yielding ManySortedSet of b₁
for b₃ being Subset of (product b₂) holds
( ex_sup_of b₃, product b₂ iff for b₄ being Element of b₁ holds ex_sup_of pi b₃,b₄,b₂ . b₄ )

proof end;

theorem Th34: :: YELLOW16:34

for b₁ being non empty set
for b₂ being non-Empty Poset-yielding ManySortedSet of b₁
for b₃ being Subset of (product b₂) holds
( ex_inf_of b₃, product b₂ iff for b₄ being Element of b₁ holds ex_inf_of pi b₃,b₄,b₂ . b₄ )

proof end;

theorem Th35: :: YELLOW16:35

for b₁ being non empty set
for b₂ being non-Empty Poset-yielding ManySortedSet of b₁
for b₃ being Subset of (product b₂) st ex_sup_of b₃, product b₂ holds
for b₄ being Element of b₁ holds (sup b₃) . b₄ = sup (pi b₃,b₄)

proof end;

theorem Th36: :: YELLOW16:36

for b₁ being non empty set
for b₂ being non-Empty Poset-yielding ManySortedSet of b₁
for b₃ being Subset of (product b₂) st ex_inf_of b₃, product b₂ holds
for b₄ being Element of b₁ holds (inf b₃) . b₄ = inf (pi b₃,b₄)

proof end;

theorem Th37: :: YELLOW16:37

for b₁ being non empty set
for b₂ being RelStr-yielding non-Empty reflexive-yielding ManySortedSet of b₁
for b₃ being directed Subset of (product b₂)
for b₄ being Element of b₁ holds pi b₃,b₄ is directed

proof end;

theorem Th38: :: YELLOW16:38

for b₁ being non empty set
for b₂, b₃ being RelStr-yielding non-Empty ManySortedSet of b₁ st ( for b₄ being Element of b₁ holds b₃ . b₄ is SubRelStr of b₂ . b₄ ) holds
product b₃ is SubRelStr of product b₂

proof end;

theorem Th39: :: YELLOW16:39

for b₁ being non empty set
for b₂, b₃ being RelStr-yielding non-Empty ManySortedSet of b₁ st ( for b₄ being Element of b₁ holds b₃ . b₄ is full SubRelStr of b₂ . b₄ ) holds
product b₃ is full SubRelStr of product b₂

proof end;

theorem Th40: :: YELLOW16:40

for b₁ being non empty RelStr
for b₂ being non empty SubRelStr of b₁
for b₃ being set holds b₂ |^ b₃ is SubRelStr of b₁ |^ b₃

proof end;

theorem Th41: :: YELLOW16:41

for b₁ being non empty RelStr
for b₂ being non empty full SubRelStr of b₁
for b₃ being set holds b₂ |^ b₃ is full SubRelStr of b₁ |^ b₃

proof end;

definition

let c₁, c₂ be non empty RelStr ;
let c₃ be set ;
pred c₁ inherits_sup_of c₃,c₂ means :Def6: :: YELLOW16:def 6
( ex_sup_of a₃,a₂ implies "\/" a₃,a₂ in the carrier of a₁ );
pred c₁ inherits_inf_of c₃,c₂ means :Def7: :: YELLOW16:def 7
( ex_inf_of a₃,a₂ implies "/\" a₃,a₂ in the carrier of a₁ );

end;

:: deftheorem Def6 defines inherits_sup_of YELLOW16:def 6 :

:: deftheorem Def7 defines inherits_inf_of YELLOW16:def 7 :

theorem Th42: :: YELLOW16:42

for b₁ being non empty transitive RelStr
for b₂ being non empty full SubRelStr of b₁
for b₃ being Subset of b₂ holds
( b₂ inherits_sup_of b₃,b₁ iff ( ex_sup_of b₃,b₁ implies ( ex_sup_of b₃,b₂ & sup b₃ = "\/" b₃,b₁ ) ) )

proof end;

theorem Th43: :: YELLOW16:43

for b₁ being non empty transitive RelStr
for b₂ being non empty full SubRelStr of b₁
for b₃ being Subset of b₂ holds
( b₂ inherits_inf_of b₃,b₁ iff ( ex_inf_of b₃,b₁ implies ( ex_inf_of b₃,b₂ & inf b₃ = "/\" b₃,b₁ ) ) )

proof end;

scheme :: YELLOW16:sch 1
s1{ F₁() -> non empty set , F₂() -> non-Empty Poset-yielding ManySortedSet of F₁(), F₃() -> non-Empty Poset-yielding ManySortedSet of F₁(), P₁[ set , set ] } :

for b₁ being Subset of (product F₃()) st P₁[b₁, product F₃()] holds
product F₃() inherits_sup_of b₁, product F₂()

provided

E40: for b₁ being Subset of (product F₃()) st P₁[b₁, product F₃()] holds
for b₂ being Element of F₁() holds P₁[ pi b₁,b₂,F₃() . b₂] and
E41: for b₁ being Element of F₁() holds F₃() . b₁ is full SubRelStr of F₂() . b₁ and
E42: for b₁ being Element of F₁()
for b₂ being Subset of (F₃() . b₁) st P₁[b₂,F₃() . b₁] holds
F₃() . b₁ inherits_sup_of b₂,F₂() . b₁

proof end;

scheme :: YELLOW16:sch 2
s2{ F₁() -> non empty set , F₂() -> non empty Poset, F₃() -> non empty full SubRelStr of F₂(), P₁[ set , set ] } :

for b₁ being Subset of (F₃() |^ F₁()) st P₁[b₁,F₃() |^ F₁()] holds
F₃() |^ F₁() inherits_sup_of b₁,F₂() |^ F₁()

provided

E40: for b₁ being Subset of (F₃() |^ F₁()) st P₁[b₁,F₃() |^ F₁()] holds
for b₂ being Element of F₁() holds P₁[ pi b₁,b₂,F₃()] and
E41: for b₁ being Subset of F₃() st P₁[b₁,F₃()] holds
F₃() inherits_sup_of b₁,F₂()

proof end;

scheme :: YELLOW16:sch 3
s3{ F₁() -> non empty set , F₂() -> non-Empty Poset-yielding ManySortedSet of F₁(), F₃() -> non-Empty Poset-yielding ManySortedSet of F₁(), P₁[ set , set ] } :

for b₁ being Subset of (product F₃()) st P₁[b₁, product F₃()] holds
product F₃() inherits_inf_of b₁, product F₂()

provided

proof end;

scheme :: YELLOW16:sch 4
s4{ F₁() -> non empty set , F₂() -> non empty Poset, F₃() -> non empty full SubRelStr of F₂(), P₁[ set , set ] } :

for b₁ being Subset of (F₃() |^ F₁()) st P₁[b₁,F₃() |^ F₁()] holds
F₃() |^ F₁() inherits_inf_of b₁,F₂() |^ F₁()

provided

proof end;

registration

let c₁ be set ;
let c₂ be non empty RelStr ;
let c₃ be non empty Subset of (c₂ |^ c₁);
let c₄ be set ;
cluster pi a₃,a₄ -> non empty ;
coherence

proof end;

end;

theorem Th44: :: YELLOW16:44

for b₁ being non empty Poset
for b₂ being non empty full directed-sups-inheriting SubRelStr of b₁
for b₃ being non empty set holds b₂ |^ b₃ is directed-sups-inheriting SubRelStr of b₁ |^ b₃

proof end;

registration

let c₁ be non empty set ;
let c₂ be RelStr-yielding non-Empty ManySortedSet of c₁;
let c₃ be non empty Subset of (product c₂);
let c₄ be set ;
cluster pi a₃,a₄ -> non empty ;
coherence

proof end;

end;

theorem Th45: :: YELLOW16:45

for b₁ being non empty set
for b₂ being non empty up-complete Poset holds b₂ |^ b₁ is up-complete

proof end;

registration

let c₁ be non empty up-complete Poset;
let c₂ be non empty set ;
cluster a₁ |^ a₂ -> up-complete ;
coherence by Th45;

end;

registration

let c₁ be TopSpace;
cluster the topology of a₁ -> non empty ;
coherence by PRE_TOPC:def 1;

end;

theorem Th46: :: YELLOW16:46

for b₁ being non empty TopSpace
for b₂ being non empty SubSpace of b₁
for b₃ being Function of b₁,b₂ st b₃ is_a_retraction holds
rng b₃ = the carrier of b₂

proof end;

theorem Th47: :: YELLOW16:47

for b₁ being non empty TopSpace
for b₂ being non empty SubSpace of b₁
for b₃ being continuous Function of b₁,b₂ st b₃ is_a_retraction holds
b₃ is idempotent

proof end;

theorem Th48: :: YELLOW16:48

for b₁ being non empty TopSpace
for b₂ being open Subset of b₁ holds chi b₂,the carrier of b₁ is continuous Function of b₁,Sierpinski_Space

proof end;

theorem Th49: :: YELLOW16:49

for b₁ being non empty TopSpace
for b₂, b₃ being Element of b₁ st ( for b₄ being open Subset of b₁ st b₃ in b₄ holds
b₂ in b₄ ) holds
0,1 --> b₃,b₂ is continuous Function of Sierpinski_Space ,b₁

proof end;

theorem Th50: :: YELLOW16:50

for b₁ being non empty TopSpace
for b₂, b₃ being Element of b₁
for b₄ being open Subset of b₁ st b₂ in b₄ & not b₃ in b₄ holds
(chi b₄,the carrier of b₁) * (0,1 --> b₃,b₂) = id Sierpinski_Space

proof end;

theorem Th51: :: YELLOW16:51

for b₁ being non empty 1-sorted
for b₂, b₃ being Subset of b₁
for b₄ being TopAugmentation of BoolePoset 1
for b₅, b₆ being Function of b₁,b₄ st b₅ = chi b₂,the carrier of b₁ & b₆ = chi b₃,the carrier of b₁ holds
( b₂ c= b₃ iff b₅ <= b₆ )

proof end;

theorem Th52: :: YELLOW16:52

for b₁ being non empty RelStr
for b₂ being non empty set
for b₃ being non empty full SubRelStr of b₁ |^ b₂ st ( for b₄ being set holds
( b₄ is Element of b₃ iff ex b₅ being Element of b₁ st b₄ = b₂ --> b₅ ) ) holds
b₁,b₃ are_isomorphic

proof end;

theorem Th53: :: YELLOW16:53

for b₁, b₂ being non empty TopSpace holds
( b₁,b₂ are_homeomorphic iff ex b₃ being continuous Function of b₁,b₂ex b₄ being continuous Function of b₂,b₁ st
( b₃ * b₄ = id b₂ & b₄ * b₃ = id b₁ ) )

proof end;

theorem Th54: :: YELLOW16:54

for b₁, b₂, b₃ being non empty TopSpace
for b₄ being Function of b₁,b₂
for b₅ being Function of b₂,b₁
for b₆ being Function of b₂,b₃ st b₄ * b₅ = id b₂ & b₆ is_homeomorphism holds
(b₆ * b₄) * (b₅ * (b₆ " )) = id b₃

proof end;

theorem Th55: :: YELLOW16:55

for b₁, b₂, b₃ being non empty TopSpace st b₂ is_Retract_of b₁ & b₂,b₃ are_homeomorphic holds
b₃ is_Retract_of b₁

proof end;

theorem Th56: :: YELLOW16:56

for b₁ being non empty TopSpace
for b₂ being non empty SubSpace of b₁ holds incl b₂,b₁ is continuous

proof end;

theorem Th57: :: YELLOW16:57

for b₁ being non empty TopSpace
for b₂ being non empty SubSpace of b₁
for b₃ being continuous Function of b₁,b₂ st b₃ is_a_retraction holds
b₃ * (incl b₂,b₁) = id b₂

proof end;

theorem Th58: :: YELLOW16:58

for b₁ being non empty TopSpace
for b₂ being non empty SubSpace of b₁ st b₂ is_a_retract_of b₁ holds
b₂ is_Retract_of b₁

proof end;

theorem Th59: :: YELLOW16:59

for b₁, b₂ being non empty TopSpace holds
( b₁ is_Retract_of b₂ iff ex b₃ being non empty SubSpace of b₂ st
( b₃ is_a_retract_of b₂ & b₃,b₁ are_homeomorphic ) )

proof end;