:: by Grzegorz Bancerek and Adam Naumowicz

::

:: Received January 6, 2000

:: Copyright (c) 2000-2021 Association of Mizar Users

theorem Th1: :: WAYBEL29:1

for X, Y being non empty set

for Z being non empty RelStr

for S being non empty SubRelStr of Z |^ [:X,Y:]

for T being non empty SubRelStr of (Z |^ Y) |^ X

for f being Function of S,T st f is currying & f is V7() & f is onto holds

f " is uncurrying

for Z being non empty RelStr

for S being non empty SubRelStr of Z |^ [:X,Y:]

for T being non empty SubRelStr of (Z |^ Y) |^ X

for f being Function of S,T st f is currying & f is V7() & f is onto holds

f " is uncurrying

proof end;

theorem Th2: :: WAYBEL29:2

for X, Y being non empty set

for Z being non empty RelStr

for S being non empty SubRelStr of Z |^ [:X,Y:]

for T being non empty SubRelStr of (Z |^ Y) |^ X

for f being Function of T,S st f is uncurrying & f is V7() & f is onto holds

f " is currying

for Z being non empty RelStr

for S being non empty SubRelStr of Z |^ [:X,Y:]

for T being non empty SubRelStr of (Z |^ Y) |^ X

for f being Function of T,S st f is uncurrying & f is V7() & f is onto holds

f " is currying

proof end;

theorem :: WAYBEL29:3

for X, Y being non empty set

for Z being non empty Poset

for S being non empty full SubRelStr of Z |^ [:X,Y:]

for T being non empty full SubRelStr of (Z |^ Y) |^ X

for f being Function of S,T st f is currying & f is V7() & f is onto holds

f is isomorphic

for Z being non empty Poset

for S being non empty full SubRelStr of Z |^ [:X,Y:]

for T being non empty full SubRelStr of (Z |^ Y) |^ X

for f being Function of S,T st f is currying & f is V7() & f is onto holds

f is isomorphic

proof end;

theorem :: WAYBEL29:4

for X, Y being non empty set

for Z being non empty Poset

for T being non empty full SubRelStr of Z |^ [:X,Y:]

for S being non empty full SubRelStr of (Z |^ Y) |^ X

for f being Function of S,T st f is uncurrying & f is V7() & f is onto holds

f is isomorphic

for Z being non empty Poset

for T being non empty full SubRelStr of Z |^ [:X,Y:]

for S being non empty full SubRelStr of (Z |^ Y) |^ X

for f being Function of S,T st f is uncurrying & f is V7() & f is onto holds

f is isomorphic

proof end;

theorem Th5: :: WAYBEL29:5

for S1, S2, T1, T2 being RelStr st RelStr(# the carrier of S1, the InternalRel of S1 #) = RelStr(# the carrier of S2, the InternalRel of S2 #) & RelStr(# the carrier of T1, the InternalRel of T1 #) = RelStr(# the carrier of T2, the InternalRel of T2 #) holds

for f being Function of S1,T1 st f is isomorphic holds

for g being Function of S2,T2 st g = f holds

g is isomorphic

for f being Function of S1,T1 st f is isomorphic holds

for g being Function of S2,T2 st g = f holds

g is isomorphic

proof end;

:: Przywlaszczone

theorem Th6: :: WAYBEL29:6

for R, S, T being RelStr

for f being Function of R,S st f is isomorphic holds

for g being Function of S,T st g is isomorphic holds

for h being Function of R,T st h = g * f holds

h is isomorphic

for f being Function of R,S st f is isomorphic holds

for g being Function of S,T st g is isomorphic holds

for h being Function of R,T st h = g * f holds

h is isomorphic

proof end;

theorem Th7: :: WAYBEL29:7

for X, Y, X1, Y1 being TopSpace st TopStruct(# the carrier of X, the topology of X #) = TopStruct(# the carrier of X1, the topology of X1 #) & TopStruct(# the carrier of Y, the topology of Y #) = TopStruct(# the carrier of Y1, the topology of Y1 #) holds

[:X,Y:] = [:X1,Y1:]

[:X,Y:] = [:X1,Y1:]

proof end;

theorem Th8: :: WAYBEL29:8

for X being non empty TopSpace

for L being non empty up-complete Scott TopPoset

for F being non empty directed Subset of (ContMaps (X,L)) holds "\/" (F,(L |^ the carrier of X)) is continuous Function of X,L

for L being non empty up-complete Scott TopPoset

for F being non empty directed Subset of (ContMaps (X,L)) holds "\/" (F,(L |^ the carrier of X)) is continuous Function of X,L

proof end;

theorem Th9: :: WAYBEL29:9

for X being non empty TopSpace

for L being non empty up-complete Scott TopPoset holds ContMaps (X,L) is directed-sups-inheriting SubRelStr of L |^ the carrier of X

for L being non empty up-complete Scott TopPoset holds ContMaps (X,L) is directed-sups-inheriting SubRelStr of L |^ the carrier of X

proof end;

theorem Th10: :: WAYBEL29:10

for S1, S2 being TopStruct st TopStruct(# the carrier of S1, the topology of S1 #) = TopStruct(# the carrier of S2, the topology of S2 #) holds

for T1, T2 being non empty TopRelStr st TopRelStr(# the carrier of T1, the InternalRel of T1, the topology of T1 #) = TopRelStr(# the carrier of T2, the InternalRel of T2, the topology of T2 #) holds

ContMaps (S1,T1) = ContMaps (S2,T2)

for T1, T2 being non empty TopRelStr st TopRelStr(# the carrier of T1, the InternalRel of T1, the topology of T1 #) = TopRelStr(# the carrier of T2, the InternalRel of T2, the topology of T2 #) holds

ContMaps (S1,T1) = ContMaps (S2,T2)

proof end;

registration

for b_{1} being continuous complete TopLattice st b_{1} is Scott holds

( b_{1} is injective & b_{1} is T_0 )
end;

cluster TopSpace-like reflexive transitive antisymmetric Scott continuous with_suprema with_infima complete -> T_0 continuous injective complete for TopRelStr ;

coherence for b

( b

proof end;

registration

ex b_{1} being TopLattice st

( b_{1} is Scott & b_{1} is continuous & b_{1} is complete )
end;

cluster non empty TopSpace-like reflexive transitive antisymmetric Scott continuous non void with_suprema with_infima complete for TopRelStr ;

existence ex b

( b

proof end;

registration

let X be non empty TopSpace;

let L be non empty up-complete Scott TopPoset;

coherence

ContMaps (X,L) is up-complete

end;
let L be non empty up-complete Scott TopPoset;

coherence

ContMaps (X,L) is up-complete

proof end;

theorem Th11: :: WAYBEL29:11

for I being non empty set

for J being non-Empty Poset-yielding ManySortedSet of I st ( for i being Element of I holds J . i is up-complete ) holds

I -POS_prod J is up-complete

for J being non-Empty Poset-yielding ManySortedSet of I st ( for i being Element of I holds J . i is up-complete ) holds

I -POS_prod J is up-complete

proof end;

theorem :: WAYBEL29:12

for I being non empty set

for J being non-Empty Poset-yielding ManySortedSet of I st ( for i being Element of I holds

( J . i is up-complete & J . i is lower-bounded ) ) holds

for x, y being Element of (product J) holds

( x << y iff ( ( for i being Element of I holds x . i << y . i ) & ex K being finite Subset of I st

for i being Element of I st not i in K holds

x . i = Bottom (J . i) ) )

for J being non-Empty Poset-yielding ManySortedSet of I st ( for i being Element of I holds

( J . i is up-complete & J . i is lower-bounded ) ) holds

for x, y being Element of (product J) holds

( x << y iff ( ( for i being Element of I holds x . i << y . i ) & ex K being finite Subset of I st

for i being Element of I st not i in K holds

x . i = Bottom (J . i) ) )

proof end;

registration

let X be set ;

let L be non empty reflexive antisymmetric lower-bounded RelStr ;

coherence

L |^ X is lower-bounded

end;
let L be non empty reflexive antisymmetric lower-bounded RelStr ;

coherence

L |^ X is lower-bounded

proof end;

registration

let X be non empty TopSpace;

let L be non empty lower-bounded TopPoset;

coherence

ContMaps (X,L) is lower-bounded

end;
let L be non empty lower-bounded TopPoset;

coherence

ContMaps (X,L) is lower-bounded

proof end;

registration

let L be non empty up-complete Poset;

coherence

for b_{1} being TopAugmentation of L holds b_{1} is up-complete

for b_{1} being TopAugmentation of L st b_{1} is Scott holds

b_{1} is correct

end;
coherence

for b

proof end;

coherence for b

b

proof end;

registration

let L be non empty up-complete Poset;

ex b_{1} being TopAugmentation of L st

( b_{1} is strict & b_{1} is Scott )

end;
cluster non empty reflexive transitive antisymmetric up-complete strict Scott non void for TopAugmentation of L;

existence ex b

( b

proof end;

theorem Th13: :: WAYBEL29:13

for L being non empty up-complete Poset

for S1, S2 being Scott TopAugmentation of L holds the topology of S1 = the topology of S2

for S1, S2 being Scott TopAugmentation of L holds the topology of S1 = the topology of S2

proof end;

theorem Th14: :: WAYBEL29:14

for S1, S2 being non empty reflexive antisymmetric up-complete TopRelStr st TopRelStr(# the carrier of S1, the InternalRel of S1, the topology of S1 #) = TopRelStr(# the carrier of S2, the InternalRel of S2, the topology of S2 #) & S1 is Scott holds

S2 is Scott

S2 is Scott

proof end;

definition

let L be non empty up-complete Poset;

uniqueness

for b_{1}, b_{2} being strict Scott TopAugmentation of L holds b_{1} = b_{2}

ex b_{1} being strict Scott TopAugmentation of L st verum
;

end;
uniqueness

for b

proof end;

existence ex b

:: deftheorem Def1 defines Sigma WAYBEL29:def 1 :

for L being non empty up-complete Poset

for b_{2} being strict Scott TopAugmentation of L holds

( b_{2} = Sigma L iff verum );

for L being non empty up-complete Poset

for b

( b

theorem Th15: :: WAYBEL29:15

for S being non empty up-complete Scott TopPoset holds Sigma S = TopRelStr(# the carrier of S, the InternalRel of S, the topology of S #)

proof end;

theorem Th16: :: WAYBEL29:16

for L1, L2 being non empty up-complete Poset st RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) holds

Sigma L1 = Sigma L2

Sigma L1 = Sigma L2

proof end;

definition

let S, T be non empty up-complete Poset;

let f be Function of S,T;

coherence

f is Function of (Sigma S),(Sigma T)

end;
let f be Function of S,T;

coherence

f is Function of (Sigma S),(Sigma T)

proof end;

:: deftheorem defines Sigma WAYBEL29:def 2 :

for S, T being non empty up-complete Poset

for f being Function of S,T holds Sigma f = f;

for S, T being non empty up-complete Poset

for f being Function of S,T holds Sigma f = f;

registration

let S, T be non empty up-complete Poset;

let f be directed-sups-preserving Function of S,T;

coherence

Sigma f is continuous

end;
let f be directed-sups-preserving Function of S,T;

coherence

Sigma f is continuous

proof end;

theorem :: WAYBEL29:17

for S, T being non empty up-complete Poset

for f being Function of S,T holds

( f is isomorphic iff Sigma f is isomorphic )

for f being Function of S,T holds

( f is isomorphic iff Sigma f is isomorphic )

proof end;

theorem Th18: :: WAYBEL29:18

for X being non empty TopSpace

for S being Scott complete TopLattice holds oContMaps (X,S) = ContMaps (X,S)

for S being Scott complete TopLattice holds oContMaps (X,S) = ContMaps (X,S)

proof end;

definition

let X, Y be non empty TopSpace;

ex b_{1} being Function of (InclPoset the topology of [:X,Y:]),(ContMaps (X,(Sigma (InclPoset the topology of Y)))) st

for W being open Subset of [:X,Y:] holds b_{1} . W = (W, the carrier of X) *graph

uniqueness

for b_{1}, b_{2} being Function of (InclPoset the topology of [:X,Y:]),(ContMaps (X,(Sigma (InclPoset the topology of Y)))) st ( for W being open Subset of [:X,Y:] holds b_{1} . W = (W, the carrier of X) *graph ) & ( for W being open Subset of [:X,Y:] holds b_{2} . W = (W, the carrier of X) *graph ) holds

b_{1} = b_{2};

end;
func Theta (X,Y) -> Function of (InclPoset the topology of [:X,Y:]),(ContMaps (X,(Sigma (InclPoset the topology of Y)))) means :Def3: :: WAYBEL29:def 3

for W being open Subset of [:X,Y:] holds it . W = (W, the carrier of X) *graph ;

existence for W being open Subset of [:X,Y:] holds it . W = (W, the carrier of X) *graph ;

ex b

for W being open Subset of [:X,Y:] holds b

proof end;

correctness uniqueness

for b

b

proof end;

:: deftheorem Def3 defines Theta WAYBEL29:def 3 :

for X, Y being non empty TopSpace

for b_{3} being Function of (InclPoset the topology of [:X,Y:]),(ContMaps (X,(Sigma (InclPoset the topology of Y)))) holds

( b_{3} = Theta (X,Y) iff for W being open Subset of [:X,Y:] holds b_{3} . W = (W, the carrier of X) *graph );

for X, Y being non empty TopSpace

for b

( b

defpred S

for L being Scott continuous complete TopLattice

for T being Scott TopAugmentation of ContMaps ($1,L) ex f being Function of (ContMaps (X,T)),(ContMaps ([:X,$1:],L)) ex g being Function of (ContMaps ([:X,$1:],L)),(ContMaps (X,T)) st

( f is uncurrying & f is V7() & f is onto & g is currying & g is V7() & g is onto );

defpred S

for L being Scott continuous complete TopLattice

for T being Scott TopAugmentation of ContMaps ($1,L) ex f being Function of (ContMaps (X,T)),(ContMaps ([:X,$1:],L)) ex g being Function of (ContMaps ([:X,$1:],L)),(ContMaps (X,T)) st

( f is uncurrying & f is isomorphic & g is currying & g is isomorphic );

defpred S

defpred S

for T being Scott TopAugmentation of InclPoset the topology of $1

for f being continuous Function of X,T holds *graph f is open Subset of [:X,$1:];

defpred S

defpred S

for y being Element of $1

for V being open a_neighborhood of y ex H being open Subset of S st

( V in H & meet H is a_neighborhood of y );

Lm1: for T being T_0-TopSpace holds

( S

proof end;

definition

let X be non empty TopSpace;

ex b_{1} being Function of (oContMaps (X,Sierpinski_Space)),(InclPoset the topology of X) st

for g being continuous Function of X,Sierpinski_Space holds b_{1} . g = g " {1}

for b_{1}, b_{2} being Function of (oContMaps (X,Sierpinski_Space)),(InclPoset the topology of X) st ( for g being continuous Function of X,Sierpinski_Space holds b_{1} . g = g " {1} ) & ( for g being continuous Function of X,Sierpinski_Space holds b_{2} . g = g " {1} ) holds

b_{1} = b_{2}

end;
func alpha X -> Function of (oContMaps (X,Sierpinski_Space)),(InclPoset the topology of X) means :Def4: :: WAYBEL29:def 4

for g being continuous Function of X,Sierpinski_Space holds it . g = g " {1};

existence for g being continuous Function of X,Sierpinski_Space holds it . g = g " {1};

ex b

for g being continuous Function of X,Sierpinski_Space holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def4 defines alpha WAYBEL29:def 4 :

for X being non empty TopSpace

for b_{2} being Function of (oContMaps (X,Sierpinski_Space)),(InclPoset the topology of X) holds

( b_{2} = alpha X iff for g being continuous Function of X,Sierpinski_Space holds b_{2} . g = g " {1} );

for X being non empty TopSpace

for b

( b

theorem :: WAYBEL29:19

for X being non empty TopSpace

for V being open Subset of X holds ((alpha X) ") . V = chi (V, the carrier of X)

for V being open Subset of X holds ((alpha X) ") . V = chi (V, the carrier of X)

proof end;

registration
end;

registration
end;

registration

let M be non empty set ;

let S be injective T_0-TopSpace;

coherence

M -TOP_prod (M => S) is injective

end;
let S be injective T_0-TopSpace;

coherence

M -TOP_prod (M => S) is injective

proof end;

theorem :: WAYBEL29:21

for M being non empty set

for L being continuous complete LATTICE holds Omega (M -TOP_prod (M => (Sigma L))) = Sigma (M -POS_prod (M => L))

for L being continuous complete LATTICE holds Omega (M -TOP_prod (M => (Sigma L))) = Sigma (M -POS_prod (M => L))

proof end;

theorem :: WAYBEL29:22

for M being non empty set

for T being injective T_0-TopSpace holds Omega (M -TOP_prod (M => T)) = Sigma (M -POS_prod (M => (Omega T)))

for T being injective T_0-TopSpace holds Omega (M -TOP_prod (M => T)) = Sigma (M -POS_prod (M => (Omega T)))

proof end;

definition

let M be non empty set ;

let X, Y be non empty TopSpace;

for b_{1}, b_{2} being Function of (oContMaps (X,(M -TOP_prod (M => Y)))),((oContMaps (X,Y)) |^ M) st ( for f being continuous Function of X,(M -TOP_prod (M => Y)) holds b_{1} . f = commute f ) & ( for f being continuous Function of X,(M -TOP_prod (M => Y)) holds b_{2} . f = commute f ) holds

b_{1} = b_{2}

ex b_{1} being Function of (oContMaps (X,(M -TOP_prod (M => Y)))),((oContMaps (X,Y)) |^ M) st

for f being continuous Function of X,(M -TOP_prod (M => Y)) holds b_{1} . f = commute f

end;
let X, Y be non empty TopSpace;

func commute (X,M,Y) -> Function of (oContMaps (X,(M -TOP_prod (M => Y)))),((oContMaps (X,Y)) |^ M) means :Def5: :: WAYBEL29:def 5

for f being continuous Function of X,(M -TOP_prod (M => Y)) holds it . f = commute f;

uniqueness for f being continuous Function of X,(M -TOP_prod (M => Y)) holds it . f = commute f;

for b

b

proof end;

existence ex b

for f being continuous Function of X,(M -TOP_prod (M => Y)) holds b

proof end;

:: deftheorem Def5 defines commute WAYBEL29:def 5 :

for M being non empty set

for X, Y being non empty TopSpace

for b_{4} being Function of (oContMaps (X,(M -TOP_prod (M => Y)))),((oContMaps (X,Y)) |^ M) holds

( b_{4} = commute (X,M,Y) iff for f being continuous Function of X,(M -TOP_prod (M => Y)) holds b_{4} . f = commute f );

for M being non empty set

for X, Y being non empty TopSpace

for b

( b

registration

let M be non empty set ;

let X, Y be non empty TopSpace;

correctness

coherence

( commute (X,M,Y) is one-to-one & commute (X,M,Y) is onto );

end;
let X, Y be non empty TopSpace;

correctness

coherence

( commute (X,M,Y) is one-to-one & commute (X,M,Y) is onto );

proof end;

registration

let M be non empty set ;

let X be non empty TopSpace;

correctness

coherence

commute (X,M,Sierpinski_Space) is isomorphic ;

end;
let X be non empty TopSpace;

correctness

coherence

commute (X,M,Sierpinski_Space) is isomorphic ;

proof end;

Lm2: for T being T_0-TopSpace st S

S

proof end;

theorem Th23: :: WAYBEL29:23

for X, Y being non empty TopSpace

for S being Scott TopAugmentation of InclPoset the topology of Y

for f1, f2 being Element of (ContMaps (X,S)) st f1 <= f2 holds

*graph f1 c= *graph f2

for S being Scott TopAugmentation of InclPoset the topology of Y

for f1, f2 being Element of (ContMaps (X,S)) st f1 <= f2 holds

*graph f1 c= *graph f2

proof end;

Lm3: for T being T_0-TopSpace st S

S

proof end;

Lm4: for T being T_0-TopSpace st S

S

proof end;

Lm5: for T being T_0-TopSpace st S

S

proof end;

Lm6: for T being T_0-TopSpace st S

S

proof end;

Lm7: for T being T_0-TopSpace st S

InclPoset the topology of T is continuous

proof end;

Lm8: for T being T_0-TopSpace st InclPoset the topology of T is continuous holds

S

proof end;

:: 4.10. THEOREM, (1) <=> (1'), pp. 131-133

theorem :: WAYBEL29:24

for Y being T_0-TopSpace holds

( ( for X being non empty TopSpace

for L being Scott continuous complete TopLattice

for T being Scott TopAugmentation of ContMaps (Y,L) ex f being Function of (ContMaps (X,T)),(ContMaps ([:X,Y:],L)) ex g being Function of (ContMaps ([:X,Y:],L)),(ContMaps (X,T)) st

( f is uncurrying & f is V7() & f is onto & g is currying & g is V7() & g is onto ) ) iff for X being non empty TopSpace

for L being Scott continuous complete TopLattice

for T being Scott TopAugmentation of ContMaps (Y,L) ex f being Function of (ContMaps (X,T)),(ContMaps ([:X,Y:],L)) ex g being Function of (ContMaps ([:X,Y:],L)),(ContMaps (X,T)) st

( f is uncurrying & f is isomorphic & g is currying & g is isomorphic ) ) by Lm1;

( ( for X being non empty TopSpace

for L being Scott continuous complete TopLattice

for T being Scott TopAugmentation of ContMaps (Y,L) ex f being Function of (ContMaps (X,T)),(ContMaps ([:X,Y:],L)) ex g being Function of (ContMaps ([:X,Y:],L)),(ContMaps (X,T)) st

( f is uncurrying & f is V7() & f is onto & g is currying & g is V7() & g is onto ) ) iff for X being non empty TopSpace

for L being Scott continuous complete TopLattice

for T being Scott TopAugmentation of ContMaps (Y,L) ex f being Function of (ContMaps (X,T)),(ContMaps ([:X,Y:],L)) ex g being Function of (ContMaps ([:X,Y:],L)),(ContMaps (X,T)) st

( f is uncurrying & f is isomorphic & g is currying & g is isomorphic ) ) by Lm1;

:: 4.10. THEOREM, (6) <=> (2), pp. 131-133

theorem :: WAYBEL29:25

for Y being T_0-TopSpace holds

( InclPoset the topology of Y is continuous iff for X being non empty TopSpace holds Theta (X,Y) is isomorphic )

( InclPoset the topology of Y is continuous iff for X being non empty TopSpace holds Theta (X,Y) is isomorphic )

proof end;

:: 4.10. THEOREM, (6) <=> (3), pp. 131-133

theorem :: WAYBEL29:26

for Y being T_0-TopSpace holds

( InclPoset the topology of Y is continuous iff for X being non empty TopSpace

for f being continuous Function of X,(Sigma (InclPoset the topology of Y)) holds *graph f is open Subset of [:X,Y:] )

( InclPoset the topology of Y is continuous iff for X being non empty TopSpace

for f being continuous Function of X,(Sigma (InclPoset the topology of Y)) holds *graph f is open Subset of [:X,Y:] )

proof end;

:: 4.10. THEOREM, (6) <=> (4), pp. 131-133

theorem :: WAYBEL29:27

for Y being T_0-TopSpace holds

( InclPoset the topology of Y is continuous iff { [W,y] where W is open Subset of Y, y is Element of Y : y in W } is open Subset of [:(Sigma (InclPoset the topology of Y)),Y:] )

( InclPoset the topology of Y is continuous iff { [W,y] where W is open Subset of Y, y is Element of Y : y in W } is open Subset of [:(Sigma (InclPoset the topology of Y)),Y:] )

proof end;

:: 4.10. THEOREM, (6) <=> (5), pp. 131-133

theorem :: WAYBEL29:28

for Y being T_0-TopSpace holds

( InclPoset the topology of Y is continuous iff for y being Element of Y

for V being open a_neighborhood of y ex H being open Subset of (Sigma (InclPoset the topology of Y)) st

( V in H & meet H is a_neighborhood of y ) )

( InclPoset the topology of Y is continuous iff for y being Element of Y

for V being open a_neighborhood of y ex H being open Subset of (Sigma (InclPoset the topology of Y)) st

( V in H & meet H is a_neighborhood of y ) )

proof end;

defpred S

defpred S

for S being complete LATTICE

for SS being Scott TopAugmentation of S holds sigma [:S,$1:] = the topology of [:SS,SL:];

defpred S

for S being complete LATTICE

for SS being Scott TopAugmentation of S

for SSL being Scott TopAugmentation of [:S,$1:] holds TopStruct(# the carrier of SSL, the topology of SSL #) = [:SS,SL:];

Lm9: for L being complete LATTICE holds

( S

proof end;

theorem :: WAYBEL29:29

for R1, R2, R3 being non empty RelStr

for f1 being Function of R1,R3 st f1 is isomorphic holds

for f2 being Function of R2,R3 st f2 = f1 & f2 is isomorphic holds

RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #)

for f1 being Function of R1,R3 st f1 is isomorphic holds

for f2 being Function of R2,R3 st f2 = f1 & f2 is isomorphic holds

RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #)

proof end;

Lm10: for L being complete LATTICE st S

S

proof end;

Lm11: for L being complete LATTICE st S

S

proof end;

:: 4.11. THEOREM, (1) <=> (2), p. 133.

theorem Th30: :: WAYBEL29:30

for L being complete LATTICE holds

( InclPoset (sigma L) is continuous iff for S being complete LATTICE holds sigma [:S,L:] = the topology of [:(Sigma S),(Sigma L):] )

( InclPoset (sigma L) is continuous iff for S being complete LATTICE holds sigma [:S,L:] = the topology of [:(Sigma S),(Sigma L):] )

proof end;

:: 4.11. THEOREM, (2) <=> (3), p. 133.

theorem Th31: :: WAYBEL29:31

for L being complete LATTICE holds

( ( for S being complete LATTICE holds sigma [:S,L:] = the topology of [:(Sigma S),(Sigma L):] ) iff for S being complete LATTICE holds TopStruct(# the carrier of (Sigma [:S,L:]), the topology of (Sigma [:S,L:]) #) = [:(Sigma S),(Sigma L):] )

( ( for S being complete LATTICE holds sigma [:S,L:] = the topology of [:(Sigma S),(Sigma L):] ) iff for S being complete LATTICE holds TopStruct(# the carrier of (Sigma [:S,L:]), the topology of (Sigma [:S,L:]) #) = [:(Sigma S),(Sigma L):] )

proof end;

:: 4.11. THEOREM, (2) <=> (3+), p. 133.

theorem Th32: :: WAYBEL29:32

for L being complete LATTICE holds

( ( for S being complete LATTICE holds sigma [:S,L:] = the topology of [:(Sigma S),(Sigma L):] ) iff for S being complete LATTICE holds Sigma [:S,L:] = Omega [:(Sigma S),(Sigma L):] )

( ( for S being complete LATTICE holds sigma [:S,L:] = the topology of [:(Sigma S),(Sigma L):] ) iff for S being complete LATTICE holds Sigma [:S,L:] = Omega [:(Sigma S),(Sigma L):] )

proof end;

:: 4.11. THEOREM, (1) <=> (3+), p. 133.

theorem :: WAYBEL29:33

for L being complete LATTICE holds

( InclPoset (sigma L) is continuous iff for S being complete LATTICE holds Sigma [:S,L:] = Omega [:(Sigma S),(Sigma L):] )

( InclPoset (sigma L) is continuous iff for S being complete LATTICE holds Sigma [:S,L:] = Omega [:(Sigma S),(Sigma L):] )

proof end;