:: by Grzegorz Bancerek

::

:: Received March 9, 1998

:: Copyright (c) 1998-2012 Association of Mizar Users

begin

scheme :: YELLOW_9:sch 1

FraenkelInvolution{ F_{1}() -> non empty set , F_{2}() -> Subset of F_{1}(), F_{3}() -> Subset of F_{1}(), F_{4}( set ) -> Element of F_{1}() } :

provided

FraenkelInvolution{ F

provided

A1:
F_{3}() = { F_{4}(a) where a is Element of F_{1}() : a in F_{2}() }
and

A2: for a being Element of F_{1}() holds F_{4}(F_{4}(a)) = a

A2: for a being Element of F

proof end;

scheme :: YELLOW_9:sch 2

FraenkelComplement1{ F_{1}() -> non empty RelStr , F_{2}() -> Subset-Family of F_{1}(), F_{3}() -> set , F_{4}( set ) -> Subset of F_{1}() } :

provided

FraenkelComplement1{ F

provided

proof end;

scheme :: YELLOW_9:sch 3

FraenkelComplement2{ F_{1}() -> non empty RelStr , F_{2}() -> Subset-Family of F_{1}(), F_{3}() -> set , F_{4}( set ) -> Subset of F_{1}() } :

provided

FraenkelComplement2{ F

provided

proof end;

theorem :: YELLOW_9:1

for R being non empty RelStr

for x, y being Element of R holds

( y in (uparrow x) ` iff not x <= y )

for x, y being Element of R holds

( y in (uparrow x) ` iff not x <= y )

proof end;

theorem Th2: :: YELLOW_9:2

for S being 1-sorted

for T being non empty 1-sorted

for f being Function of S,T

for X being Subset of T holds (f " X) ` = f " (X `)

for T being non empty 1-sorted

for f being Function of S,T

for X being Subset of T holds (f " X) ` = f " (X `)

proof end;

theorem Th3: :: YELLOW_9:3

for T being 1-sorted

for F being Subset-Family of T holds COMPLEMENT F = { (a `) where a is Subset of T : a in F }

for F being Subset-Family of T holds COMPLEMENT F = { (a `) where a is Subset of T : a in F }

proof end;

theorem Th4: :: YELLOW_9:4

for R being non empty RelStr

for F being Subset of R holds

( uparrow F = union { (uparrow x) where x is Element of R : x in F } & downarrow F = union { (downarrow x) where x is Element of R : x in F } )

for F being Subset of R holds

( uparrow F = union { (uparrow x) where x is Element of R : x in F } & downarrow F = union { (downarrow x) where x is Element of R : x in F } )

proof end;

theorem :: YELLOW_9:5

for R being non empty RelStr

for A being Subset-Family of R

for F being Subset of R st A = { ((uparrow x) `) where x is Element of R : x in F } holds

Intersect A = (uparrow F) `

for A being Subset-Family of R

for F being Subset of R st A = { ((uparrow x) `) where x is Element of R : x in F } holds

Intersect A = (uparrow F) `

proof end;

registration

ex b_{1} being TopLattice st

( b_{1} is strict & b_{1} is complete & b_{1} is 1 -element )
end;

cluster non empty 1 -element correct reflexive transitive antisymmetric with_suprema with_infima complete strict for TopRelStr ;

existence ex b

( b

proof end;

registration

let S be non empty RelStr ;

let T be non empty reflexive antisymmetric upper-bounded RelStr ;

ex b_{1} being Function of S,T st b_{1} is infs-preserving

end;
let T be non empty reflexive antisymmetric upper-bounded RelStr ;

cluster non empty Relation-like the carrier of S -defined the carrier of T -valued Function-like V27( the carrier of S) quasi_total infs-preserving for Element of bool [: the carrier of S, the carrier of T:];

existence ex b

proof end;

registration

let S be non empty RelStr ;

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

ex b_{1} being Function of S,T st b_{1} is sups-preserving

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

cluster non empty Relation-like the carrier of S -defined the carrier of T -valued Function-like V27( the carrier of S) quasi_total sups-preserving for Element of bool [: the carrier of S, the carrier of T:];

existence ex b

proof end;

definition

let R, S be 1-sorted ;

assume A1: the carrier of S c= the carrier of R ;

A2: dom (id the carrier of S) = the carrier of S ;

A3: rng (id the carrier of S) = the carrier of S ;

coherence

id the carrier of S is Function of S,R by A1, A2, A3, FUNCT_2:2;

end;
assume A1: the carrier of S c= the carrier of R ;

A2: dom (id the carrier of S) = the carrier of S ;

A3: rng (id the carrier of S) = the carrier of S ;

coherence

id the carrier of S is Function of S,R by A1, A2, A3, FUNCT_2:2;

:: deftheorem Def1 defines incl YELLOW_9:def 1 :

for R, S being 1-sorted st the carrier of S c= the carrier of R holds

incl (S,R) = id the carrier of S;

for R, S being 1-sorted st the carrier of S c= the carrier of R holds

incl (S,R) = id the carrier of S;

registration

let R be non empty RelStr ;

let S be non empty SubRelStr of R;

coherence

incl (S,R) is monotone

end;
let S be non empty SubRelStr of R;

coherence

incl (S,R) is monotone

proof end;

definition

let R be non empty RelStr ;

let X be non empty Subset of R;

(incl ((subrelstr X),R)) * ((subrelstr X) +id) is non empty strict NetStr over R ;

(incl ((subrelstr X),R)) * ((subrelstr X) opp+id) is non empty strict NetStr over R ;

end;
let X be non empty Subset of R;

func X +id -> non empty strict NetStr over R equals :: YELLOW_9:def 2

(incl ((subrelstr X),R)) * ((subrelstr X) +id);

coherence (incl ((subrelstr X),R)) * ((subrelstr X) +id);

(incl ((subrelstr X),R)) * ((subrelstr X) +id) is non empty strict NetStr over R ;

func X opp+id -> non empty strict NetStr over R equals :: YELLOW_9:def 3

(incl ((subrelstr X),R)) * ((subrelstr X) opp+id);

coherence (incl ((subrelstr X),R)) * ((subrelstr X) opp+id);

(incl ((subrelstr X),R)) * ((subrelstr X) opp+id) is non empty strict NetStr over R ;

:: deftheorem defines +id YELLOW_9:def 2 :

for R being non empty RelStr

for X being non empty Subset of R holds X +id = (incl ((subrelstr X),R)) * ((subrelstr X) +id);

for R being non empty RelStr

for X being non empty Subset of R holds X +id = (incl ((subrelstr X),R)) * ((subrelstr X) +id);

:: deftheorem defines opp+id YELLOW_9:def 3 :

for R being non empty RelStr

for X being non empty Subset of R holds X opp+id = (incl ((subrelstr X),R)) * ((subrelstr X) opp+id);

for R being non empty RelStr

for X being non empty Subset of R holds X opp+id = (incl ((subrelstr X),R)) * ((subrelstr X) opp+id);

theorem :: YELLOW_9:6

for R being non empty RelStr

for X being non empty Subset of R holds

( the carrier of (X +id) = X & X +id is full SubRelStr of R & ( for x being Element of (X +id) holds (X +id) . x = x ) )

for X being non empty Subset of R holds

( the carrier of (X +id) = X & X +id is full SubRelStr of R & ( for x being Element of (X +id) holds (X +id) . x = x ) )

proof end;

theorem :: YELLOW_9:7

for R being non empty RelStr

for X being non empty Subset of R holds

( the carrier of (X opp+id) = X & X opp+id is full SubRelStr of R opp & ( for x being Element of (X opp+id) holds (X opp+id) . x = x ) )

for X being non empty Subset of R holds

( the carrier of (X opp+id) = X & X opp+id is full SubRelStr of R opp & ( for x being Element of (X opp+id) holds (X opp+id) . x = x ) )

proof end;

registration

let R be non empty reflexive RelStr ;

let X be non empty Subset of R;

coherence

X +id is reflexive ;

coherence

X opp+id is reflexive ;

end;
let X be non empty Subset of R;

coherence

X +id is reflexive ;

coherence

X opp+id is reflexive ;

registration

let R be non empty transitive RelStr ;

let X be non empty Subset of R;

coherence

X +id is transitive ;

coherence

X opp+id is transitive ;

end;
let X be non empty Subset of R;

coherence

X +id is transitive ;

coherence

X opp+id is transitive ;

registration

let R be non empty reflexive RelStr ;

let I be directed Subset of R;

coherence

subrelstr I is directed

end;
let I be directed Subset of R;

coherence

subrelstr I is directed

proof end;

registration

let R be non empty reflexive RelStr ;

let I be non empty directed Subset of R;

coherence

I +id is directed ;

end;
let I be non empty directed Subset of R;

coherence

I +id is directed ;

registration

let R be non empty reflexive RelStr ;

let F be non empty filtered Subset of R;

coherence

(subrelstr F) opp+id is directed

end;
let F be non empty filtered Subset of R;

coherence

(subrelstr F) opp+id is directed

proof end;

registration

let R be non empty reflexive RelStr ;

let F be non empty filtered Subset of R;

coherence

F opp+id is directed ;

end;
let F be non empty filtered Subset of R;

coherence

F opp+id is directed ;

begin

theorem Th9: :: YELLOW_9:9

for T being 1 -element TopSpace holds

( the topology of T = bool the carrier of T & ( for x being Point of T holds

( the carrier of T = {x} & the topology of T = {{},{x}} ) ) )

( the topology of T = bool the carrier of T & ( for x being Point of T holds

( the carrier of T = {x} & the topology of T = {{},{x}} ) ) )

proof end;

theorem :: YELLOW_9:10

for T being 1 -element TopSpace holds

( { the carrier of T} is Basis of T & {} is prebasis of T & {{}} is prebasis of T )

( { the carrier of T} is Basis of T & {} is prebasis of T & {{}} is prebasis of T )

proof end;

theorem Th11: :: YELLOW_9:11

for X, Y being set

for A being Subset-Family of X st A = {Y} holds

( FinMeetCl A = {Y,X} & UniCl A = {Y,{}} )

for A being Subset-Family of X st A = {Y} holds

( FinMeetCl A = {Y,X} & UniCl A = {Y,{}} )

proof end;

theorem :: YELLOW_9:12

for X being set

for A, B being Subset-Family of X st ( A = B \/ {X} or B = A \ {X} ) holds

Intersect A = Intersect B

for A, B being Subset-Family of X st ( A = B \/ {X} or B = A \ {X} ) holds

Intersect A = Intersect B

proof end;

theorem :: YELLOW_9:13

for X being set

for A, B being Subset-Family of X st ( A = B \/ {X} or B = A \ {X} ) holds

FinMeetCl A = FinMeetCl B

for A, B being Subset-Family of X st ( A = B \/ {X} or B = A \ {X} ) holds

FinMeetCl A = FinMeetCl B

proof end;

theorem Th14: :: YELLOW_9:14

for X being set

for A being Subset-Family of X st X in A holds

for x being set holds

( x in FinMeetCl A iff ex Y being non empty finite Subset-Family of X st

( Y c= A & x = Intersect Y ) )

for A being Subset-Family of X st X in A holds

for x being set holds

( x in FinMeetCl A iff ex Y being non empty finite Subset-Family of X st

( Y c= A & x = Intersect Y ) )

proof end;

theorem Th18: :: YELLOW_9:18

for X being set

for A being Subset-Family of X st A = {{},X} holds

( UniCl A = A & FinMeetCl A = A )

for A being Subset-Family of X st A = {{},X} holds

( UniCl A = A & FinMeetCl A = A )

proof end;

theorem Th19: :: YELLOW_9:19

for X, Y being set

for A being Subset-Family of X

for B being Subset-Family of Y holds

( ( A c= B implies UniCl A c= UniCl B ) & ( A = B implies UniCl A = UniCl B ) )

for A being Subset-Family of X

for B being Subset-Family of Y holds

( ( A c= B implies UniCl A c= UniCl B ) & ( A = B implies UniCl A = UniCl B ) )

proof end;

theorem Th20: :: YELLOW_9:20

for X, Y being set

for A being Subset-Family of X

for B being Subset-Family of Y st A = B & X in A holds

FinMeetCl B = {Y} \/ (FinMeetCl A)

for A being Subset-Family of X

for B being Subset-Family of Y st A = B & X in A holds

FinMeetCl B = {Y} \/ (FinMeetCl A)

proof end;

theorem Th21: :: YELLOW_9:21

for X being set

for A being Subset-Family of X holds UniCl (FinMeetCl (UniCl A)) = UniCl (FinMeetCl A)

for A being Subset-Family of X holds UniCl (FinMeetCl (UniCl A)) = UniCl (FinMeetCl A)

proof end;

begin

theorem Th22: :: YELLOW_9:22

for T being TopSpace

for K being Subset-Family of T holds

( the topology of T = UniCl K iff K is Basis of T )

for K being Subset-Family of T holds

( the topology of T = UniCl K iff K is Basis of T )

proof end;

theorem Th23: :: YELLOW_9:23

for T being TopSpace

for K being Subset-Family of T holds

( K is prebasis of T iff FinMeetCl K is Basis of T )

for K being Subset-Family of T holds

( K is prebasis of T iff FinMeetCl K is Basis of T )

proof end;

theorem Th24: :: YELLOW_9:24

for T being non empty TopSpace

for B being Subset-Family of T st UniCl B is prebasis of T holds

B is prebasis of T

for B being Subset-Family of T st UniCl B is prebasis of T holds

B is prebasis of T

proof end;

theorem Th25: :: YELLOW_9:25

for T1, T2 being TopSpace

for B being Basis of T1 st the carrier of T1 = the carrier of T2 & B is Basis of T2 holds

the topology of T1 = the topology of T2

for B being Basis of T1 st the carrier of T1 = the carrier of T2 & B is Basis of T2 holds

the topology of T1 = the topology of T2

proof end;

theorem Th26: :: YELLOW_9:26

for T1, T2 being TopSpace

for P being prebasis of T1 st the carrier of T1 = the carrier of T2 & P is prebasis of T2 holds

the topology of T1 = the topology of T2

for P being prebasis of T1 st the carrier of T1 = the carrier of T2 & P is prebasis of T2 holds

the topology of T1 = the topology of T2

proof end;

theorem :: YELLOW_9:27

theorem Th29: :: YELLOW_9:29

for T being non empty TopSpace

for B being prebasis of T holds B \/ { the carrier of T} is prebasis of T

for B being prebasis of T holds B \/ { the carrier of T} is prebasis of T

proof end;

theorem Th31: :: YELLOW_9:31

for T being TopSpace

for B being Basis of T

for A being Subset of T holds

( A is open iff for p being Point of T st p in A holds

ex a being Subset of T st

( a in B & p in a & a c= A ) )

for B being Basis of T

for A being Subset of T holds

( A is open iff for p being Point of T st p in A holds

ex a being Subset of T st

( a in B & p in a & a c= A ) )

proof end;

theorem Th32: :: YELLOW_9:32

for T being TopSpace

for B being Subset-Family of T st B c= the topology of T & ( for A being Subset of T st A is open holds

for p being Point of T st p in A holds

ex a being Subset of T st

( a in B & p in a & a c= A ) ) holds

B is Basis of T

for B being Subset-Family of T st B c= the topology of T & ( for A being Subset of T st A is open holds

for p being Point of T st p in A holds

ex a being Subset of T st

( a in B & p in a & a c= A ) ) holds

B is Basis of T

proof end;

theorem Th33: :: YELLOW_9:33

for S being TopSpace

for T being non empty TopSpace

for K being Basis of T

for f being Function of S,T holds

( f is continuous iff for A being Subset of T st A in K holds

f " (A `) is closed )

for T being non empty TopSpace

for K being Basis of T

for f being Function of S,T holds

( f is continuous iff for A being Subset of T st A in K holds

f " (A `) is closed )

proof end;

theorem :: YELLOW_9:34

for S being TopSpace

for T being non empty TopSpace

for K being Basis of T

for f being Function of S,T holds

( f is continuous iff for A being Subset of T st A in K holds

f " A is open )

for T being non empty TopSpace

for K being Basis of T

for f being Function of S,T holds

( f is continuous iff for A being Subset of T st A in K holds

f " A is open )

proof end;

theorem Th35: :: YELLOW_9:35

for S being TopSpace

for T being non empty TopSpace

for K being prebasis of T

for f being Function of S,T holds

( f is continuous iff for A being Subset of T st A in K holds

f " (A `) is closed )

for T being non empty TopSpace

for K being prebasis of T

for f being Function of S,T holds

( f is continuous iff for A being Subset of T st A in K holds

f " (A `) is closed )

proof end;

theorem :: YELLOW_9:36

for S being TopSpace

for T being non empty TopSpace

for K being prebasis of T

for f being Function of S,T holds

( f is continuous iff for A being Subset of T st A in K holds

f " A is open )

for T being non empty TopSpace

for K being prebasis of T

for f being Function of S,T holds

( f is continuous iff for A being Subset of T st A in K holds

f " A is open )

proof end;

theorem Th37: :: YELLOW_9:37

for T being non empty TopSpace

for x being Point of T

for X being Subset of T

for K being Basis of T st ( for A being Subset of T st A in K & x in A holds

A meets X ) holds

x in Cl X

for x being Point of T

for X being Subset of T

for K being Basis of T st ( for A being Subset of T st A in K & x in A holds

A meets X ) holds

x in Cl X

proof end;

theorem Th38: :: YELLOW_9:38

for T being non empty TopSpace

for x being Point of T

for X being Subset of T

for K being prebasis of T st ( for Z being finite Subset-Family of T st Z c= K & x in Intersect Z holds

Intersect Z meets X ) holds

x in Cl X

for x being Point of T

for X being Subset of T

for K being prebasis of T st ( for Z being finite Subset-Family of T st Z c= K & x in Intersect Z holds

Intersect Z meets X ) holds

x in Cl X

proof end;

theorem :: YELLOW_9:39

for T being non empty TopSpace

for K being prebasis of T

for x being Point of T

for N being net of T st ( for A being Subset of T st A in K & x in A holds

N is_eventually_in A ) holds

for S being Subset of T st rng (netmap (N,T)) c= S holds

x in Cl S

for K being prebasis of T

for x being Point of T

for N being net of T st ( for A being Subset of T st A in K & x in A holds

N is_eventually_in A ) holds

for S being Subset of T st rng (netmap (N,T)) c= S holds

x in Cl S

proof end;

begin

theorem Th40: :: YELLOW_9:40

for T1, T2 being non empty TopSpace

for B1 being Basis of T1

for B2 being Basis of T2 holds { [:a,b:] where a is Subset of T1, b is Subset of T2 : ( a in B1 & b in B2 ) } is Basis of [:T1,T2:]

for B1 being Basis of T1

for B2 being Basis of T2 holds { [:a,b:] where a is Subset of T1, b is Subset of T2 : ( a in B1 & b in B2 ) } is Basis of [:T1,T2:]

proof end;

theorem Th41: :: YELLOW_9:41

for T1, T2 being non empty TopSpace

for B1 being prebasis of T1

for B2 being prebasis of T2 holds { [: the carrier of T1,b:] where b is Subset of T2 : b in B2 } \/ { [:a, the carrier of T2:] where a is Subset of T1 : a in B1 } is prebasis of [:T1,T2:]

for B1 being prebasis of T1

for B2 being prebasis of T2 holds { [: the carrier of T1,b:] where b is Subset of T2 : b in B2 } \/ { [:a, the carrier of T2:] where a is Subset of T1 : a in B1 } is prebasis of [:T1,T2:]

proof end;

theorem :: YELLOW_9:42

for X1, X2 being set

for A being Subset-Family of [:X1,X2:]

for A1 being non empty Subset-Family of X1

for A2 being non empty Subset-Family of X2 st A = { [:a,b:] where a is Subset of X1, b is Subset of X2 : ( a in A1 & b in A2 ) } holds

Intersect A = [:(Intersect A1),(Intersect A2):]

for A being Subset-Family of [:X1,X2:]

for A1 being non empty Subset-Family of X1

for A2 being non empty Subset-Family of X2 st A = { [:a,b:] where a is Subset of X1, b is Subset of X2 : ( a in A1 & b in A2 ) } holds

Intersect A = [:(Intersect A1),(Intersect A2):]

proof end;

theorem :: YELLOW_9:43

for T1, T2 being non empty TopSpace

for B1 being prebasis of T1

for B2 being prebasis of T2 st union B1 = the carrier of T1 & union B2 = the carrier of T2 holds

{ [:a,b:] where a is Subset of T1, b is Subset of T2 : ( a in B1 & b in B2 ) } is prebasis of [:T1,T2:]

for B1 being prebasis of T1

for B2 being prebasis of T2 st union B1 = the carrier of T1 & union B2 = the carrier of T2 holds

{ [:a,b:] where a is Subset of T1, b is Subset of T2 : ( a in B1 & b in B2 ) } is prebasis of [:T1,T2:]

proof end;

begin

definition

let R be RelStr ;

ex b_{1} being TopRelStr st RelStr(# the carrier of b_{1}, the InternalRel of b_{1} #) = RelStr(# the carrier of R, the InternalRel of R #)

end;
mode TopAugmentation of R -> TopRelStr means :Def4: :: YELLOW_9:def 4

RelStr(# the carrier of it, the InternalRel of it #) = RelStr(# the carrier of R, the InternalRel of R #);

existence RelStr(# the carrier of it, the InternalRel of it #) = RelStr(# the carrier of R, the InternalRel of R #);

ex b

proof end;

:: deftheorem Def4 defines TopAugmentation YELLOW_9:def 4 :

for R being RelStr

for b_{2} being TopRelStr holds

( b_{2} is TopAugmentation of R iff RelStr(# the carrier of b_{2}, the InternalRel of b_{2} #) = RelStr(# the carrier of R, the InternalRel of R #) );

for R being RelStr

for b

( b

registration

let R be RelStr ;

existence

ex b_{1} being TopAugmentation of R st

( b_{1} is correct & b_{1} is discrete & b_{1} is strict )

end;
existence

ex b

( b

proof end;

theorem :: YELLOW_9:46

for R being RelStr

for T1 being TopAugmentation of R

for T2 being TopAugmentation of T1 holds T2 is TopAugmentation of R

for T1 being TopAugmentation of R

for T2 being TopAugmentation of T1 holds T2 is TopAugmentation of R

proof end;

registration

let R be non empty RelStr ;

coherence

for b_{1} being TopAugmentation of R holds not b_{1} is empty

end;
coherence

for b

proof end;

registration

let R be reflexive RelStr ;

coherence

for b_{1} being TopAugmentation of R holds b_{1} is reflexive

end;
coherence

for b

proof end;

registration

let R be transitive RelStr ;

coherence

for b_{1} being TopAugmentation of R holds b_{1} is transitive

end;
coherence

for b

proof end;

registration

let R be antisymmetric RelStr ;

coherence

for b_{1} being TopAugmentation of R holds b_{1} is antisymmetric

end;
coherence

for b

proof end;

registration

let R be non empty complete RelStr ;

coherence

for b_{1} being TopAugmentation of R holds b_{1} is complete

end;
coherence

for b

proof end;

theorem Th47: :: YELLOW_9:47

for S being non empty reflexive antisymmetric up-complete RelStr

for T being non empty reflexive RelStr st RelStr(# the carrier of S, the InternalRel of S #) = RelStr(# the carrier of T, the InternalRel of T #) holds

for A being Subset of S

for C being Subset of T st A = C & A is inaccessible holds

C is inaccessible

for T being non empty reflexive RelStr st RelStr(# the carrier of S, the InternalRel of S #) = RelStr(# the carrier of T, the InternalRel of T #) holds

for A being Subset of S

for C being Subset of T st A = C & A is inaccessible holds

C is inaccessible

proof end;

theorem Th48: :: YELLOW_9:48

for S being non empty reflexive RelStr

for T being TopAugmentation of S st the topology of T = sigma S holds

T is correct

for T being TopAugmentation of S st the topology of T = sigma S holds

T is correct

proof end;

theorem Th49: :: YELLOW_9:49

for S being complete LATTICE

for T being TopAugmentation of S st the topology of T = sigma S holds

T is Scott

for T being TopAugmentation of S st the topology of T = sigma S holds

T is Scott

proof end;

registration

let R be complete LATTICE;

ex b_{1} being TopAugmentation of R st

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

end;
cluster non empty correct reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V194() up-complete /\-complete strict Scott for TopAugmentation of R;

existence ex b

( b

proof end;

theorem Th50: :: YELLOW_9:50

for S, T being non empty reflexive transitive antisymmetric complete Scott TopRelStr st RelStr(# the carrier of S, the InternalRel of S #) = RelStr(# the carrier of T, the InternalRel of T #) holds

for F being Subset of S

for G being Subset of T st F = G & F is open holds

G is open

for F being Subset of S

for G being Subset of T st F = G & F is open holds

G is open

proof end;

theorem Th51: :: YELLOW_9:51

for S being complete LATTICE

for T being Scott TopAugmentation of S holds the topology of T = sigma S

for T being Scott TopAugmentation of S holds the topology of T = sigma S

proof end;

theorem :: YELLOW_9:52

for S, T being complete LATTICE st RelStr(# the carrier of S, the InternalRel of S #) = RelStr(# the carrier of T, the InternalRel of T #) holds

sigma S = sigma T

sigma S = sigma T

proof end;

registration

let R be complete LATTICE;

coherence

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

b_{1} is correct

end;
coherence

for b

b

proof end;

Lm1: for S being TopStruct ex T being strict TopSpace st

( the carrier of T = the carrier of S & the topology of S is prebasis of T )

proof end;

begin

definition

let T be TopStruct ;

ex b_{1} being TopSpace st

( the carrier of T = the carrier of b_{1} & the topology of T c= the topology of b_{1} )

end;
mode TopExtension of T -> TopSpace means :Def5: :: YELLOW_9:def 5

( the carrier of T = the carrier of it & the topology of T c= the topology of it );

existence ( the carrier of T = the carrier of it & the topology of T c= the topology of it );

ex b

( the carrier of T = the carrier of b

proof end;

:: deftheorem Def5 defines TopExtension YELLOW_9:def 5 :

for T being TopStruct

for b_{2} being TopSpace holds

( b_{2} is TopExtension of T iff ( the carrier of T = the carrier of b_{2} & the topology of T c= the topology of b_{2} ) );

for T being TopStruct

for b

( b

theorem Th53: :: YELLOW_9:53

for S being TopStruct ex T being TopExtension of S st

( T is strict & the topology of S is prebasis of T )

( T is strict & the topology of S is prebasis of T )

proof end;

registration

let T be TopStruct ;

existence

ex b_{1} being TopExtension of T st

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

end;
existence

ex b

( b

proof end;

definition

let T1, T2 be TopStruct ;

ex b_{1} being TopSpace st

( the carrier of b_{1} = the carrier of T1 \/ the carrier of T2 & the topology of T1 \/ the topology of T2 is prebasis of b_{1} )

end;
mode Refinement of T1,T2 -> TopSpace means :Def6: :: YELLOW_9:def 6

( the carrier of it = the carrier of T1 \/ the carrier of T2 & the topology of T1 \/ the topology of T2 is prebasis of it );

existence ( the carrier of it = the carrier of T1 \/ the carrier of T2 & the topology of T1 \/ the topology of T2 is prebasis of it );

ex b

( the carrier of b

proof end;

:: deftheorem Def6 defines Refinement YELLOW_9:def 6 :

for T1, T2 being TopStruct

for b_{3} being TopSpace holds

( b_{3} is Refinement of T1,T2 iff ( the carrier of b_{3} = the carrier of T1 \/ the carrier of T2 & the topology of T1 \/ the topology of T2 is prebasis of b_{3} ) );

for T1, T2 being TopStruct

for b

( b

registration

let T1 be non empty TopStruct ;

let T2 be TopStruct ;

coherence

for b_{1} being Refinement of T1,T2 holds not b_{1} is empty

for b_{1} being Refinement of T2,T1 holds not b_{1} is empty

end;
let T2 be TopStruct ;

coherence

for b

proof end;

coherence for b

proof end;

theorem :: YELLOW_9:54

for T1, T2 being TopStruct

for T, T9 being Refinement of T1,T2 holds TopStruct(# the carrier of T, the topology of T #) = TopStruct(# the carrier of T9, the topology of T9 #)

for T, T9 being Refinement of T1,T2 holds TopStruct(# the carrier of T, the topology of T #) = TopStruct(# the carrier of T9, the topology of T9 #)

proof end;

theorem :: YELLOW_9:56

for T1, T2 being TopStruct

for T being Refinement of T1,T2

for X being Subset-Family of T st X = the topology of T1 \/ the topology of T2 holds

the topology of T = UniCl (FinMeetCl X)

for T being Refinement of T1,T2

for X being Subset-Family of T st X = the topology of T1 \/ the topology of T2 holds

the topology of T = UniCl (FinMeetCl X)

proof end;

theorem :: YELLOW_9:57

for T1, T2 being TopStruct st the carrier of T1 = the carrier of T2 holds

for T being Refinement of T1,T2 holds

( T is TopExtension of T1 & T is TopExtension of T2 )

for T being Refinement of T1,T2 holds

( T is TopExtension of T1 & T is TopExtension of T2 )

proof end;

theorem :: YELLOW_9:58

for T1, T2 being non empty TopSpace

for T being Refinement of T1,T2

for B1 being prebasis of T1

for B2 being prebasis of T2 holds (B1 \/ B2) \/ { the carrier of T1, the carrier of T2} is prebasis of T

for T being Refinement of T1,T2

for B1 being prebasis of T1

for B2 being prebasis of T2 holds (B1 \/ B2) \/ { the carrier of T1, the carrier of T2} is prebasis of T

proof end;

theorem Th59: :: YELLOW_9:59

for T1, T2 being non empty TopSpace

for B1 being Basis of T1

for B2 being Basis of T2

for T being Refinement of T1,T2 holds (B1 \/ B2) \/ (INTERSECTION (B1,B2)) is Basis of T

for B1 being Basis of T1

for B2 being Basis of T2

for T being Refinement of T1,T2 holds (B1 \/ B2) \/ (INTERSECTION (B1,B2)) is Basis of T

proof end;

theorem Th60: :: YELLOW_9:60

for T1, T2 being non empty TopSpace st the carrier of T1 = the carrier of T2 holds

for T being Refinement of T1,T2 holds INTERSECTION ( the topology of T1, the topology of T2) is Basis of T

for T being Refinement of T1,T2 holds INTERSECTION ( the topology of T1, the topology of T2) is Basis of T

proof end;

theorem :: YELLOW_9:61

for L being non empty RelStr

for T1, T2 being correct TopAugmentation of L

for T being Refinement of T1,T2 holds INTERSECTION ( the topology of T1, the topology of T2) is Basis of T

for T1, T2 being correct TopAugmentation of L

for T being Refinement of T1,T2 holds INTERSECTION ( the topology of T1, the topology of T2) is Basis of T

proof end;