:: YELLOW_9 semantic presentation

scheme :: YELLOW_9:sch 1
s1{ F₁() -> non empty set , F₂() -> Subset of F₁(), F₃() -> Subset of F₁(), F₄( set ) -> Element of F₁() } :

F₂() = { F₄(b₁) where B is Element of F₁() : b₁ in F₃() }

provided

E1: F₃() = { F₄(b₁) where B is Element of F₁() : b₁ in F₂() } and
E2: for b₁ being Element of F₁() holds F₄(F₄(b₁)) = b₁

proof end;

scheme :: YELLOW_9:sch 2
s2{ F₁() -> non empty RelStr , F₂() -> Subset-Family of F₁(), F₃() -> set , F₄( set ) -> Subset of F₁() } :

COMPLEMENT F₂() = { (F₄(b₁) ` ) where B is Element of F₁() : b₁ in F₃() }

provided

E1: F₂() = { F₄(b₁) where B is Element of F₁() : b₁ in F₃() }

proof end;

scheme :: YELLOW_9:sch 3
s3{ F₁() -> non empty RelStr , F₂() -> Subset-Family of F₁(), F₃() -> set , F₄( set ) -> Subset of F₁() } :

COMPLEMENT F₂() = { F₄(b₁) where B is Element of F₁() : b₁ in F₃() }

provided

E1: F₂() = { (F₄(b₁) ` ) where B is Element of F₁() : b₁ in F₃() }

proof end;

theorem Th1: :: YELLOW_9:1

for b₁ being non empty RelStr
for b₂, b₃ being Element of b₁ holds
( b₃ in (uparrow b₂) ` iff not b₂ <= b₃ )

proof end;

scheme :: YELLOW_9:sch 4
s4{ F₁() -> TopSpace, F₂( set ) -> set , F₃() -> Function, P₁[ set ] } :

F₃() " (union { F₂(b₁) where B is Subset of F₁() : P₁[b₁] } ) = union { (F₃() " F₂(b₁)) where B is Subset of F₁() : P₁[b₁] }

proof end;

theorem Th2: :: YELLOW_9:2

for b₁ being 1-sorted
for b₂ being non empty 1-sorted
for b₃ being Function of b₁,b₂
for b₄ being Subset of b₂ holds (b₃ " b₄) ` = b₃ " (b₄ ` )

proof end;

theorem Th3: :: YELLOW_9:3

for b₁ being 1-sorted
for b₂ being Subset-Family of b₁ holds COMPLEMENT b₂ = { (b₃ ` ) where B is Subset of b₁ : b₃ in b₂ }

proof end;

theorem Th4: :: YELLOW_9:4

for b₁ being non empty RelStr
for b₂ being Subset of b₁ holds
( uparrow b₂ = union { (uparrow b₃) where B is Element of b₁ : b₃ in b₂ } & downarrow b₂ = union { (downarrow b₃) where B is Element of b₁ : b₃ in b₂ } )

proof end;

theorem Th5: :: YELLOW_9:5

for b₁ being non empty RelStr
for b₂ being Subset-Family of b₁
for b₃ being Subset of b₁ st b₂ = { ((uparrow b₄) ` ) where B is Element of b₁ : b₄ in b₃ } holds
Intersect b₂ = (uparrow b₃) `

proof end;

Lemma4: for b₁ being Subset-Family of {0}
for b₂ being Relation of {0} st b₁ = {{} ,{0}} & b₂ = {[0,0]} holds
( TopRelStr(# {0},b₂,b₁ #) is trivial & TopRelStr(# {0},b₂,b₁ #) is reflexive & not TopRelStr(# {0},b₂,b₁ #) is empty & TopRelStr(# {0},b₂,b₁ #) is discrete & TopRelStr(# {0},b₂,b₁ #) is finite )

proof end;

registration

cluster non empty reflexive strict discrete finite trivial TopRelStr ;
existence

proof end;

end;

registration

cluster strict complete trivial TopRelStr ;
existence

proof end;

end;

registration

let c₁ be non empty RelStr ;
let c₂ be non empty reflexive antisymmetric upper-bounded RelStr ;
cluster infs-preserving Relation of the carrier of a₁,the carrier of a₂;
existence

proof end;

end;

registration

let c₁ be non empty RelStr ;
let c₂ be non empty reflexive antisymmetric lower-bounded RelStr ;
cluster sups-preserving Relation of the carrier of a₁,the carrier of a₂;
existence

proof end;

end;

definition

let c₁, c₂ be 1-sorted ;
assume E5: the carrier of c₂ c= the carrier of c₁ ;
E6: ( dom (id the carrier of c₂) = the carrier of c₂ & rng (id the carrier of c₂) = the carrier of c₂ ) by RELAT_1:71;
func incl c₂,c₁ -> Function of a₂,a₁ equals :Def1: :: YELLOW_9:def 1
id the carrier of a₂;
coherence by E5, E6, FUNCT_2:4;

end;

:: deftheorem Def1 defines incl YELLOW_9:def 1 :

registration

let c₁ be non empty RelStr ;
let c₂ be non empty SubRelStr of c₁;
cluster incl a₂,a₁ -> monotone ;
coherence

proof end;

end;

definition

let c₁ be non empty RelStr ;
let c₂ be non empty Subset of c₁;
func c₂ +id -> non empty strict NetStr of a₁ equals :: YELLOW_9:def 2
(incl (subrelstr a₂),a₁) * ((subrelstr a₂) +id );
coherence ;
func c₂ opp+id -> non empty strict NetStr of a₁ equals :: YELLOW_9:def 3
(incl (subrelstr a₂),a₁) * ((subrelstr a₂) opp+id );
coherence ;

end;

:: deftheorem Def2 defines +id YELLOW_9:def 2 :

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

theorem Th6: :: YELLOW_9:6

for b₁ being non empty RelStr
for b₂ being non empty Subset of b₁ holds
( the carrier of (b₂ +id ) = b₂ & b₂ +id is full SubRelStr of b₁ & ( for b₃ being Element of (b₂ +id ) holds (b₂ +id ) . b₃ = b₃ ) )

proof end;

theorem Th7: :: YELLOW_9:7

for b₁ being non empty RelStr
for b₂ being non empty Subset of b₁ holds
( the carrier of (b₂ opp+id ) = b₂ & b₂ opp+id is full SubRelStr of b₁ opp & ( for b₃ being Element of (b₂ opp+id ) holds (b₂ opp+id ) . b₃ = b₃ ) )

proof end;

registration

let c₁ be non empty reflexive RelStr ;
let c₂ be non empty Subset of c₁;
cluster a₂ +id -> non empty reflexive strict ;
coherence ;
cluster a₂ opp+id -> non empty reflexive strict ;
coherence ;

end;

registration

let c₁ be non empty transitive RelStr ;
let c₂ be non empty Subset of c₁;
cluster a₂ +id -> non empty transitive strict ;
coherence ;
cluster a₂ opp+id -> non empty transitive strict ;
coherence ;

end;

registration

let c₁ be non empty reflexive RelStr ;
let c₂ be directed Subset of c₁;
cluster subrelstr a₂ -> directed ;
coherence

proof end;

end;

registration

let c₁ be non empty reflexive RelStr ;
let c₂ be non empty directed Subset of c₁;
cluster a₂ +id -> non empty reflexive strict directed ;
coherence ;

end;

registration

let c₁ be non empty reflexive RelStr ;
let c₂ be non empty filtered Subset of c₁;
cluster (subrelstr a₂) opp+id -> directed ;
coherence

proof end;

end;

registration

let c₁ be non empty reflexive RelStr ;
let c₂ be non empty filtered Subset of c₁;
cluster a₂ opp+id -> non empty reflexive strict directed ;
coherence ;

end;

theorem Th8: :: YELLOW_9:8

for b₁ being TopSpace st b₁ is empty holds
the topology of b₁ = {{} }

proof end;

theorem Th9: :: YELLOW_9:9

for b₁ being non empty trivial TopSpace holds
( the topology of b₁ = bool the carrier of b₁ & ( for b₂ being Point of b₁ holds
( the carrier of b₁ = {b₂} & the topology of b₁ = {{} ,{b₂}} ) ) )

proof end;

theorem Th10: :: YELLOW_9:10

for b₁ being non empty trivial TopSpace holds
( {the carrier of b₁} is Basis of b₁ & {} is prebasis of b₁ & {{} } is prebasis of b₁ )

proof end;

theorem Th11: :: YELLOW_9:11

for b₁, b₂ being set
for b₃ being Subset-Family of b₁ st b₃ = {b₂} holds
( FinMeetCl b₃ = {b₂,b₁} & UniCl b₃ = {b₂,{} } )

proof end;

theorem Th12: :: YELLOW_9:12

for b₁ being set
for b₂, b₃ being Subset-Family of b₁ st ( b₂ = b₃ \/ {b₁} or b₃ = b₂ \ {b₁} ) holds
Intersect b₂ = Intersect b₃

proof end;

theorem Th13: :: YELLOW_9:13

for b₁ being set
for b₂, b₃ being Subset-Family of b₁ st ( b₂ = b₃ \/ {b₁} or b₃ = b₂ \ {b₁} ) holds
FinMeetCl b₂ = FinMeetCl b₃

proof end;

theorem Th14: :: YELLOW_9:14

for b₁ being set
for b₂ being Subset-Family of b₁ st b₁ in b₂ holds
for b₃ being set holds
( b₃ in FinMeetCl b₂ iff ex b₄ being non empty finite Subset-Family of b₁ st
( b₄ c= b₂ & b₃ = Intersect b₄ ) )

proof end;

theorem Th15: :: YELLOW_9:15

for b₁ being set
for b₂ being Subset-Family of b₁ holds UniCl (UniCl b₂) = UniCl b₂

proof end;

theorem Th16: :: YELLOW_9:16

for b₁ being set
for b₂ being empty Subset-Family of b₁ holds UniCl b₂ = {{} }

proof end;

theorem Th17: :: YELLOW_9:17

for b₁ being set
for b₂ being empty Subset-Family of b₁ holds FinMeetCl b₂ = {b₁}

proof end;

theorem Th18: :: YELLOW_9:18

for b₁ being set
for b₂ being Subset-Family of b₁ st b₂ = {{} ,b₁} holds
( UniCl b₂ = b₂ & FinMeetCl b₂ = b₂ )

proof end;

theorem Th19: :: YELLOW_9:19

for b₁, b₂ being set
for b₃ being Subset-Family of b₁
for b₄ being Subset-Family of b₂ holds
( ( b₃ c= b₄ implies UniCl b₃ c= UniCl b₄ ) & ( b₃ = b₄ implies UniCl b₃ = UniCl b₄ ) )

proof end;

theorem Th20: :: YELLOW_9:20

for b₁, b₂ being set
for b₃ being Subset-Family of b₁
for b₄ being Subset-Family of b₂ st b₃ = b₄ & b₁ in b₃ & b₁ c= b₂ holds
FinMeetCl b₄ = {b₂} \/ (FinMeetCl b₃)

proof end;

theorem Th21: :: YELLOW_9:21

for b₁ being set
for b₂ being Subset-Family of b₁ holds UniCl (FinMeetCl (UniCl b₂)) = UniCl (FinMeetCl b₂)

proof end;

theorem Th22: :: YELLOW_9:22

for b₁ being TopSpace
for b₂ being Subset-Family of b₁ holds
( the topology of b₁ = UniCl b₂ iff b₂ is Basis of b₁ )

proof end;

theorem Th23: :: YELLOW_9:23

for b₁ being TopSpace
for b₂ being Subset-Family of b₁ holds
( b₂ is prebasis of b₁ iff FinMeetCl b₂ is Basis of b₁ )

proof end;

theorem Th24: :: YELLOW_9:24

for b₁ being non empty TopSpace
for b₂ being Subset-Family of b₁ st UniCl b₂ is prebasis of b₁ holds
b₂ is prebasis of b₁

proof end;

theorem Th25: :: YELLOW_9:25

for b₁, b₂ being TopSpace
for b₃ being Basis of b₁ st the carrier of b₁ = the carrier of b₂ & b₃ is Basis of b₂ holds
the topology of b₁ = the topology of b₂

proof end;

theorem Th26: :: YELLOW_9:26

for b₁, b₂ being TopSpace
for b₃ being prebasis of b₁ st the carrier of b₁ = the carrier of b₂ & b₃ is prebasis of b₂ holds
the topology of b₁ = the topology of b₂

proof end;

theorem Th27: :: YELLOW_9:27

for b₁ being TopSpace
for b₂ being Basis of b₁ holds
( b₂ is open & b₂ is prebasis of b₁ )

proof end;

theorem Th28: :: YELLOW_9:28

for b₁ being TopSpace
for b₂ being prebasis of b₁ holds b₂ is open

proof end;

theorem Th29: :: YELLOW_9:29

for b₁ being non empty TopSpace
for b₂ being prebasis of b₁ holds b₂ \/ {the carrier of b₁} is prebasis of b₁

proof end;

theorem Th30: :: YELLOW_9:30

for b₁ being TopSpace
for b₂ being Basis of b₁ holds b₂ \/ {the carrier of b₁} is Basis of b₁

proof end;

theorem Th31: :: YELLOW_9:31

for b₁ being TopSpace
for b₂ being Basis of b₁
for b₃ being Subset of b₁ holds
( b₃ is open iff for b₄ being Point of b₁ st b₄ in b₃ holds
ex b₅ being Subset of b₁ st
( b₅ in b₂ & b₄ in b₅ & b₅ c= b₃ ) )

proof end;

theorem Th32: :: YELLOW_9:32

for b₁ being TopSpace
for b₂ being Subset-Family of b₁ st b₂ c= the topology of b₁ & ( for b₃ being Subset of b₁ st b₃ is open holds
for b₄ being Point of b₁ st b₄ in b₃ holds
ex b₅ being Subset of b₁ st
( b₅ in b₂ & b₄ in b₅ & b₅ c= b₃ ) ) holds
b₂ is Basis of b₁

proof end;

theorem Th33: :: YELLOW_9:33

for b₁ being TopSpace
for b₂ being non empty TopSpace
for b₃ being Basis of b₂
for b₄ being Function of b₁,b₂ holds
( b₄ is continuous iff for b₅ being Subset of b₂ st b₅ in b₃ holds
b₄ " (b₅ ` ) is closed )

proof end;

theorem Th34: :: YELLOW_9:34

for b₁ being TopSpace
for b₂ being non empty TopSpace
for b₃ being Basis of b₂
for b₄ being Function of b₁,b₂ holds
( b₄ is continuous iff for b₅ being Subset of b₂ st b₅ in b₃ holds
b₄ " b₅ is open )

proof end;

theorem Th35: :: YELLOW_9:35

for b₁ being TopSpace
for b₂ being non empty TopSpace
for b₃ being prebasis of b₂
for b₄ being Function of b₁,b₂ holds
( b₄ is continuous iff for b₅ being Subset of b₂ st b₅ in b₃ holds
b₄ " (b₅ ` ) is closed )

proof end;

theorem Th36: :: YELLOW_9:36

proof end;

theorem Th37: :: YELLOW_9:37

for b₁ being non empty TopSpace
for b₂ being Point of b₁
for b₃ being Subset of b₁
for b₄ being Basis of b₁ st ( for b₅ being Subset of b₁ st b₅ in b₄ & b₂ in b₅ holds
b₅ meets b₃ ) holds
b₂ in Cl b₃

proof end;

theorem Th38: :: YELLOW_9:38

for b₁ being non empty TopSpace
for b₂ being Point of b₁
for b₃ being Subset of b₁
for b₄ being prebasis of b₁ st ( for b₅ being finite Subset-Family of b₁ st b₅ c= b₄ & b₂ in Intersect b₅ holds
Intersect b₅ meets b₃ ) holds
b₂ in Cl b₃

proof end;

theorem Th39: :: YELLOW_9:39

for b₁ being non empty TopSpace
for b₂ being prebasis of b₁
for b₃ being Point of b₁
for b₄ being net of b₁ st ( for b₅ being Subset of b₁ st b₅ in b₂ & b₃ in b₅ holds
b₄ is_eventually_in b₅ ) holds
for b₅ being Subset of b₁ st rng (netmap b₄,b₁) c= b₅ holds
b₃ in Cl b₅

proof end;

theorem Th40: :: YELLOW_9:40

for b₁, b₂ being non empty TopSpace
for b₃ being Basis of b₁
for b₄ being Basis of b₂ holds { [:b₅,b₆:] where B is Subset of b₁, B is Subset of b₂ : ( b₅ in b₃ & b₆ in b₄ ) } is Basis of [:b₁,b₂:]

proof end;

theorem Th41: :: YELLOW_9:41

for b₁, b₂ being non empty TopSpace
for b₃ being prebasis of b₁
for b₄ being prebasis of b₂ holds { [:the carrier of b₁,b₅:] where B is Subset of b₂ : b₅ in b₄ } \/ { [:b₅,the carrier of b₂:] where B is Subset of b₁ : b₅ in b₃ } is prebasis of [:b₁,b₂:]

proof end;

theorem Th42: :: YELLOW_9:42

for b₁, b₂ being set
for b₃ being Subset-Family of [:b₁,b₂:]
for b₄ being non empty Subset-Family of b₁
for b₅ being non empty Subset-Family of b₂ st b₃ = { [:b₆,b₇:] where B is Subset of b₁, B is Subset of b₂ : ( b₆ in b₄ & b₇ in b₅ ) } holds
Intersect b₃ = [:(Intersect b₄),(Intersect b₅):]

proof end;

theorem Th43: :: YELLOW_9:43

for b₁, b₂ being non empty TopSpace
for b₃ being prebasis of b₁
for b₄ being prebasis of b₂ st union b₃ = the carrier of b₁ & union b₄ = the carrier of b₂ holds
{ [:b₅,b₆:] where B is Subset of b₁, B is Subset of b₂ : ( b₅ in b₃ & b₆ in b₄ ) } is prebasis of [:b₁,b₂:]

proof end;

definition

let c₁ be RelStr ;
mode TopAugmentation of c₁ -> TopRelStr means :Def4: :: YELLOW_9:def 4
RelStr(# the carrier of a₂,the InternalRel of a₂ #) = RelStr(# the carrier of a₁,the InternalRel of a₁ #);
existence

proof end;

end;

:: deftheorem Def4 defines TopAugmentation YELLOW_9:def 4 :

notation

let c₁ be RelStr ;
let c₂ be TopAugmentation of c₁;
synonym correct c₂ for TopSpace-like c₁;

end;

registration

let c₁ be RelStr ;
cluster correct strict discrete TopAugmentation of a₁;
existence

proof end;

end;

theorem Th44: :: YELLOW_9:44

for b₁ being TopRelStr holds b₁ is TopAugmentation of b₁

proof end;

theorem Th45: :: YELLOW_9:45

for b₁ being TopRelStr
for b₂ being TopAugmentation of b₁ holds b₁ is TopAugmentation of b₂

proof end;

theorem Th46: :: YELLOW_9:46

for b₁ being RelStr
for b₂ being TopAugmentation of b₁
for b₃ being TopAugmentation of b₂ holds b₃ is TopAugmentation of b₁

proof end;

registration

let c₁ be non empty RelStr ;
cluster -> non empty TopAugmentation of a₁;
coherence

proof end;

end;

registration

let c₁ be reflexive RelStr ;
cluster -> reflexive TopAugmentation of a₁;
coherence

proof end;

end;

registration

let c₁ be transitive RelStr ;
cluster -> transitive TopAugmentation of a₁;
coherence

proof end;

end;

registration

let c₁ be antisymmetric RelStr ;
cluster -> antisymmetric TopAugmentation of a₁;
coherence

proof end;

end;

registration

let c₁ be non empty complete RelStr ;
cluster -> non empty complete TopAugmentation of a₁;
coherence

proof end;

end;

theorem Th47: :: YELLOW_9:47

for b₁ being non empty reflexive antisymmetric up-complete RelStr
for b₂ being non empty reflexive RelStr st RelStr(# the carrier of b₁,the InternalRel of b₁ #) = RelStr(# the carrier of b₂,the InternalRel of b₂ #) holds
for b₃ being Subset of b₁
for b₄ being Subset of b₂ st b₃ = b₄ & b₃ is inaccessible_by_directed_joins holds
b₄ is inaccessible_by_directed_joins

proof end;

theorem Th48: :: YELLOW_9:48

for b₁ being non empty reflexive RelStr
for b₂ being TopAugmentation of b₁ st the topology of b₂ = sigma b₁ holds
b₂ is correct

proof end;

theorem Th49: :: YELLOW_9:49

for b₁ being complete LATTICE
for b₂ being TopAugmentation of b₁ st the topology of b₂ = sigma b₁ holds
b₂ is Scott

proof end;

registration

let c₁ be complete LATTICE;
cluster non empty correct reflexive transitive antisymmetric strict Scott complete TopAugmentation of a₁;
existence

proof end;

end;

theorem Th50: :: YELLOW_9:50

for b₁, b₂ being non empty reflexive transitive antisymmetric Scott complete TopRelStr st RelStr(# the carrier of b₁,the InternalRel of b₁ #) = RelStr(# the carrier of b₂,the InternalRel of b₂ #) holds
for b₃ being Subset of b₁
for b₄ being Subset of b₂ st b₃ = b₄ & b₃ is open holds
b₄ is open

proof end;

theorem Th51: :: YELLOW_9:51

for b₁ being complete LATTICE
for b₂ being Scott TopAugmentation of b₁ holds the topology of b₂ = sigma b₁

proof end;

theorem Th52: :: YELLOW_9:52

for b₁, b₂ being complete LATTICE st RelStr(# the carrier of b₁,the InternalRel of b₁ #) = RelStr(# the carrier of b₂,the InternalRel of b₂ #) holds
sigma b₁ = sigma b₂

proof end;

registration

let c₁ be complete LATTICE;
cluster Scott -> non empty correct reflexive transitive antisymmetric complete TopAugmentation of a₁;
coherence

proof end;

end;

Lemma37: for b₁ being TopStruct ex b₂ being strict TopSpace st
( the carrier of b₂ = the carrier of b₁ & the topology of b₁ is prebasis of b₂ )

proof end;

definition

let c₁ be TopStruct ;
mode TopExtension of c₁ -> TopSpace means :Def5: :: YELLOW_9:def 5
( the carrier of a₁ = the carrier of a₂ & the topology of a₁ c= the topology of a₂ );
existence

proof end;

end;

:: deftheorem Def5 defines TopExtension YELLOW_9:def 5 :

theorem Th53: :: YELLOW_9:53

for b₁ being TopStruct ex b₂ being TopExtension of b₁ st
( b₂ is strict & the topology of b₁ is prebasis of b₂ )

proof end;

registration

let c₁ be TopStruct ;
cluster strict discrete TopExtension of a₁;
existence

proof end;

end;

definition

let c₁, c₂ be TopStruct ;
mode Refinement of c₁,c₂ -> TopSpace means :Def6: :: YELLOW_9:def 6
( the carrier of a₃ = the carrier of a₁ \/ the carrier of a₂ & the topology of a₁ \/ the topology of a₂ is prebasis of a₃ );
existence

proof end;

end;

:: deftheorem Def6 defines Refinement YELLOW_9:def 6 :

registration

let c₁ be non empty TopStruct ;
let c₂ be TopStruct ;
cluster -> non empty Refinement of a₁,a₂;
coherence

proof end;

cluster -> non empty Refinement of a₂,a₁;
coherence

proof end;

end;

theorem Th54: :: YELLOW_9:54

for b₁, b₂ being TopStruct
for b₃, b₄ being Refinement of b₁,b₂ holds TopStruct(# the carrier of b₃,the topology of b₃ #) = TopStruct(# the carrier of b₄,the topology of b₄ #)

proof end;

theorem Th55: :: YELLOW_9:55

for b₁, b₂ being TopStruct
for b₃ being Refinement of b₁,b₂ holds b₃ is Refinement of b₂,b₁

proof end;

theorem Th56: :: YELLOW_9:56

for b₁, b₂ being TopStruct
for b₃ being Refinement of b₁,b₂
for b₄ being Subset-Family of b₃ st b₄ = the topology of b₁ \/ the topology of b₂ holds
the topology of b₃ = UniCl (FinMeetCl b₄)

proof end;

theorem Th57: :: YELLOW_9:57

for b₁, b₂ being TopStruct st the carrier of b₁ = the carrier of b₂ holds
for b₃ being Refinement of b₁,b₂ holds
( b₃ is TopExtension of b₁ & b₃ is TopExtension of b₂ )

proof end;

theorem Th58: :: YELLOW_9:58

for b₁, b₂ being non empty TopSpace
for b₃ being Refinement of b₁,b₂
for b₄ being prebasis of b₁
for b₅ being prebasis of b₂ holds (b₄ \/ b₅) \/ {the carrier of b₁,the carrier of b₂} is prebasis of b₃

proof end;

theorem Th59: :: YELLOW_9:59

for b₁, b₂ being non empty TopSpace
for b₃ being Basis of b₁
for b₄ being Basis of b₂
for b₅ being Refinement of b₁,b₂ holds (b₃ \/ b₄) \/ (INTERSECTION b₃,b₄) is Basis of b₅

proof end;

theorem Th60: :: YELLOW_9:60

for b₁, b₂ being non empty TopSpace st the carrier of b₁ = the carrier of b₂ holds
for b₃ being Refinement of b₁,b₂ holds INTERSECTION the topology of b₁,the topology of b₂ is Basis of b₃

proof end;

theorem Th61: :: YELLOW_9:61

for b₁ being non empty RelStr
for b₂, b₃ being correct TopAugmentation of b₁
for b₄ being Refinement of b₂,b₃ holds INTERSECTION the topology of b₂,the topology of b₃ is Basis of b₄

proof end;