:: TOPREAL6 semantic presentation

Lemma1: sqrt 2 > 0
by SQUARE_1:84;

theorem Th1: :: TOPREAL6:1

canceled;

theorem Th2: :: TOPREAL6:2

canceled;

theorem Th3: :: TOPREAL6:3

canceled;

theorem Th4: :: TOPREAL6:4

canceled;

theorem Th5: :: TOPREAL6:5

canceled;

theorem Th6: :: TOPREAL6:6

for b₁, b₂ being real number st 0 <= b₁ & 0 <= b₂ holds
sqrt (b₁ + b₂) <= (sqrt b₁) + (sqrt b₂)

proof end;

theorem Th7: :: TOPREAL6:7

for b₁, b₂ being real number st 0 <= b₁ & b₁ <= b₂ holds
abs b₁ <= abs b₂

proof end;

theorem Th8: :: TOPREAL6:8

for b₁, b₂ being real number st b₁ <= b₂ & b₂ <= 0 holds
abs b₂ <= abs b₁

proof end;

theorem Th9: :: TOPREAL6:9

for b₁ being Real holds Product (0 |-> b₁) = 1 by FINSEQ_2:72, RVSUM_1:124;

theorem Th10: :: TOPREAL6:10

for b₁ being Real holds Product (1 |-> b₁) = b₁

proof end;

theorem Th11: :: TOPREAL6:11

for b₁ being Real holds Product (2 |-> b₁) = b₁ * b₁

proof end;

theorem Th12: :: TOPREAL6:12

for b₁ being Real
for b₂ being Nat holds Product ((b₂ + 1) |-> b₁) = (Product (b₂ |-> b₁)) * b₁

proof end;

theorem Th13: :: TOPREAL6:13

for b₁ being Real
for b₂ being Nat holds
( ( b₂ <> 0 & b₁ = 0 ) iff Product (b₂ |-> b₁) = 0 )

proof end;

theorem Th14: :: TOPREAL6:14

for b₁ being Real
for b₂, b₃ being Nat st b₁ <> 0 & b₂ <= b₃ holds
Product ((b₃ -' b₂) |-> b₁) = (Product (b₃ |-> b₁)) / (Product (b₂ |-> b₁))

proof end;

theorem Th15: :: TOPREAL6:15

for b₁ being Real
for b₂, b₃ being Nat st b₁ <> 0 & b₂ <= b₃ holds
b₁ |^ (b₃ -' b₂) = (b₁ |^ b₃) / (b₁ |^ b₂)

proof end;

theorem Th16: :: TOPREAL6:16

for b₁, b₂ being Real holds sqr <*b₁,b₂*> = <*(b₁ ^2 ),(b₂ ^2 )*>

proof end;

theorem Th17: :: TOPREAL6:17

for b₁ being Nat
for b₂ being Real
for b₃ being FinSequence of REAL st b₁ in dom (abs b₃) & b₂ = b₃ . b₁ holds
(abs b₃) . b₁ = abs b₂

proof end;

theorem Th18: :: TOPREAL6:18

for b₁, b₂ being Real holds abs <*b₁,b₂*> = <*(abs b₁),(abs b₂)*>

proof end;

theorem Th19: :: TOPREAL6:19

for b₁, b₂, b₃, b₄ being real number st b₁ <= b₂ & b₃ <= b₄ holds
(abs (b₂ - b₁)) + (abs (b₄ - b₃)) = (b₂ - b₁) + (b₄ - b₃)

proof end;

theorem Th20: :: TOPREAL6:20

for b₁, b₂ being real number st b₂ > 0 holds
b₁ in ].(b₁ - b₂),(b₁ + b₂).[

proof end;

theorem Th21: :: TOPREAL6:21

for b₁, b₂ being real number st b₂ >= 0 holds
b₁ in [.(b₁ - b₂),(b₁ + b₂).]

proof end;

theorem Th22: :: TOPREAL6:22

for b₁, b₂ being real number st b₁ < b₂ holds
( inf ].b₁,b₂.[ = b₁ & sup ].b₁,b₂.[ = b₂ )

proof end;

theorem Th23: :: TOPREAL6:23

canceled;

theorem Th24: :: TOPREAL6:24

for b₁ being bounded Subset of REAL holds b₁ c= [.(inf b₁),(sup b₁).]

proof end;

registration

let c₁ be TopStruct ;
let c₂ be finite Subset of c₁;
cluster a₁ | a₂ -> finite ;
coherence

proof end;

end;

registration

cluster non empty strict finite TopStruct ;
existence

proof end;

end;

registration

let c₁ be TopStruct ;
cluster empty -> connected Element of bool the carrier of a₁;
coherence

proof end;

end;

registration

let c₁ be TopSpace;
cluster finite -> compact Element of bool the carrier of a₁;
coherence

proof end;

end;

theorem Th25: :: TOPREAL6:25

for b₁, b₂ being TopSpace st b₁,b₂ are_homeomorphic & b₁ is connected holds
b₂ is connected

proof end;

theorem Th26: :: TOPREAL6:26

for b₁ being TopSpace
for b₂ being finite Subset-Family of b₁ st ( for b₃ being Subset of b₁ st b₃ in b₂ holds
b₃ is compact ) holds
union b₂ is compact

proof end;

theorem Th27: :: TOPREAL6:27

canceled;

theorem Th28: :: TOPREAL6:28

canceled;

theorem Th29: :: TOPREAL6:29

for b₁, b₂, b₃, b₄, b₅, b₆ being set st b₁ c= b₂ & b₃ c= b₄ holds
product (b₅,b₆ --> b₁,b₃) c= product (b₅,b₆ --> b₂,b₄)

proof end;

theorem Th30: :: TOPREAL6:30

for b₁, b₂ being Subset of REAL holds product (1,2 --> b₁,b₂) is Subset of (TOP-REAL 2)

proof end;

theorem Th31: :: TOPREAL6:31

for b₁ being Real holds
( |.|[0,b₁]|.| = abs b₁ & |.|[b₁,0]|.| = abs b₁ )

proof end;

theorem Th32: :: TOPREAL6:32

for b₁ being Point of (Euclid 2)
for b₂ being Point of (TOP-REAL 2) st b₁ = 0.REAL 2 & b₁ = b₂ holds
( b₂ = <*0,0*> & b₂ `1 = 0 & b₂ `2 = 0 )

proof end;

theorem Th33: :: TOPREAL6:33

for b₁, b₂ being Point of (Euclid 2)
for b₃ being Point of (TOP-REAL 2) st b₁ = 0.REAL 2 & b₂ = b₃ holds
dist b₁,b₂ = |.b₃.|

proof end;

theorem Th34: :: TOPREAL6:34

for b₁ being Real
for b₂ being Point of (TOP-REAL 2) holds b₁ * b₂ = |[(b₁ * (b₂ `1 )),(b₁ * (b₂ `2 ))]|

proof end;

theorem Th35: :: TOPREAL6:35

for b₁ being Real
for b₂, b₃, b₄ being Point of (TOP-REAL 2) st b₂ = ((1 - b₁) * b₃) + (b₁ * b₄) & b₂ <> b₃ & 0 <= b₁ holds
0 < b₁

proof end;

theorem Th36: :: TOPREAL6:36

for b₁ being Real
for b₂, b₃, b₄ being Point of (TOP-REAL 2) st b₂ = ((1 - b₁) * b₃) + (b₁ * b₄) & b₂ <> b₄ & b₁ <= 1 holds
b₁ < 1

proof end;

theorem Th37: :: TOPREAL6:37

for b₁, b₂, b₃ being Point of (TOP-REAL 2) st b₁ in LSeg b₂,b₃ & b₁ <> b₂ & b₁ <> b₃ & b₂ `1 < b₃ `1 holds
( b₂ `1 < b₁ `1 & b₁ `1 < b₃ `1 )

proof end;

theorem Th38: :: TOPREAL6:38

for b₁, b₂, b₃ being Point of (TOP-REAL 2) st b₁ in LSeg b₂,b₃ & b₁ <> b₂ & b₁ <> b₃ & b₂ `2 < b₃ `2 holds
( b₂ `2 < b₁ `2 & b₁ `2 < b₃ `2 )

proof end;

theorem Th39: :: TOPREAL6:39

for b₁ being non empty Subset of (TOP-REAL 2)
for b₂ being Point of (TOP-REAL 2) ex b₃ being Point of (TOP-REAL 2) st
( b₃ `1 < W-bound b₁ & b₂ <> b₃ )

proof end;

theorem Th40: :: TOPREAL6:40

for b₁ being non empty Subset of (TOP-REAL 2)
for b₂ being Point of (TOP-REAL 2) ex b₃ being Point of (TOP-REAL 2) st
( b₃ `1 > E-bound b₁ & b₂ <> b₃ )

proof end;

theorem Th41: :: TOPREAL6:41

for b₁ being non empty Subset of (TOP-REAL 2)
for b₂ being Point of (TOP-REAL 2) ex b₃ being Point of (TOP-REAL 2) st
( b₃ `2 > N-bound b₁ & b₂ <> b₃ )

proof end;

theorem Th42: :: TOPREAL6:42

for b₁ being non empty Subset of (TOP-REAL 2)
for b₂ being Point of (TOP-REAL 2) ex b₃ being Point of (TOP-REAL 2) st
( b₃ `2 < S-bound b₁ & b₂ <> b₃ )

proof end;

registration

cluster non empty convex -> connected Element of bool the carrier of (TOP-REAL 2);
coherence by JORDAN1:9;
cluster non horizontal -> non empty Element of bool the carrier of (TOP-REAL 2);
coherence

proof end;

cluster non vertical -> non empty Element of bool the carrier of (TOP-REAL 2);
coherence

proof end;

cluster being_Region -> open connected Element of bool the carrier of (TOP-REAL 2);
coherence by TOPREAL4:def 3;
cluster open connected -> being_Region Element of bool the carrier of (TOP-REAL 2);
coherence by TOPREAL4:def 3;

end;

registration

cluster empty -> horizontal Element of bool the carrier of (TOP-REAL 2);
coherence

proof end;

cluster empty -> vertical Element of bool the carrier of (TOP-REAL 2);
coherence

proof end;

end;

registration

cluster non empty connected convex Element of bool the carrier of (TOP-REAL 2);
existence

proof end;

end;

registration

let c₁, c₂ be Point of (TOP-REAL 2);
cluster LSeg a₁,a₂ -> connected convex ;
coherence by GOBOARD9:7, GOBOARD9:8;

end;

registration

cluster R^2-unit_square -> connected ;
coherence

proof end;

end;

registration

cluster being_simple_closed_curve -> connected Element of bool the carrier of (TOP-REAL 2);
coherence

proof end;

end;

theorem Th43: :: TOPREAL6:43

for b₁ being Subset of (TOP-REAL 2) holds LSeg (NE-corner b₁),(SE-corner b₁) c= L~ (SpStSeq b₁)

proof end;

theorem Th44: :: TOPREAL6:44

for b₁ being Subset of (TOP-REAL 2) holds LSeg (SW-corner b₁),(SE-corner b₁) c= L~ (SpStSeq b₁)

proof end;

theorem Th45: :: TOPREAL6:45

for b₁ being Subset of (TOP-REAL 2) holds LSeg (SW-corner b₁),(NW-corner b₁) c= L~ (SpStSeq b₁)

proof end;

theorem Th46: :: TOPREAL6:46

for b₁ being Subset of (TOP-REAL 2) holds { b₂ where B is Point of (TOP-REAL 2) : b₂ `1 < W-bound b₁ } is non empty connected convex Subset of (TOP-REAL 2)

proof end;

theorem Th47: :: TOPREAL6:47

for b₁, b₂ being Point of (TOP-REAL 2)
for b₃ being Point of (Euclid 2)
for b₄ being real number st b₃ = b₁ & b₂ in Ball b₃,b₄ holds
( (b₁ `1 ) - b₄ < b₂ `1 & b₂ `1 < (b₁ `1 ) + b₄ )

proof end;

theorem Th48: :: TOPREAL6:48

for b₁, b₂ being Point of (TOP-REAL 2)
for b₃ being Point of (Euclid 2)
for b₄ being real number st b₃ = b₁ & b₂ in Ball b₃,b₄ holds
( (b₁ `2 ) - b₄ < b₂ `2 & b₂ `2 < (b₁ `2 ) + b₄ )

proof end;

theorem Th49: :: TOPREAL6:49

for b₁ being Point of (TOP-REAL 2)
for b₂ being Point of (Euclid 2)
for b₃ being real number st b₁ = b₂ holds
product (1,2 --> ].((b₁ `1 ) - (b₃ / (sqrt 2))),((b₁ `1 ) + (b₃ / (sqrt 2))).[,].((b₁ `2 ) - (b₃ / (sqrt 2))),((b₁ `2 ) + (b₃ / (sqrt 2))).[) c= Ball b₂,b₃

proof end;

theorem Th50: :: TOPREAL6:50

for b₁ being Point of (TOP-REAL 2)
for b₂ being Point of (Euclid 2)
for b₃ being real number st b₁ = b₂ holds
Ball b₂,b₃ c= product (1,2 --> ].((b₁ `1 ) - b₃),((b₁ `1 ) + b₃).[,].((b₁ `2 ) - b₃),((b₁ `2 ) + b₃).[)

proof end;

theorem Th51: :: TOPREAL6:51

for b₁ being Point of (TOP-REAL 2)
for b₂ being Point of (Euclid 2)
for b₃ being Subset of (TOP-REAL 2)
for b₄ being real number st b₃ = Ball b₂,b₄ & b₁ = b₂ holds
proj1 .: b₃ = ].((b₁ `1 ) - b₄),((b₁ `1 ) + b₄).[

proof end;

theorem Th52: :: TOPREAL6:52

for b₁ being Point of (TOP-REAL 2)
for b₂ being Point of (Euclid 2)
for b₃ being Subset of (TOP-REAL 2)
for b₄ being real number st b₃ = Ball b₂,b₄ & b₁ = b₂ holds
proj2 .: b₃ = ].((b₁ `2 ) - b₄),((b₁ `2 ) + b₄).[

proof end;

theorem Th53: :: TOPREAL6:53

for b₁ being Point of (TOP-REAL 2)
for b₂ being Point of (Euclid 2)
for b₃ being non empty Subset of (TOP-REAL 2)
for b₄ being real number st b₃ = Ball b₂,b₄ & b₁ = b₂ holds
W-bound b₃ = (b₁ `1 ) - b₄

proof end;

theorem Th54: :: TOPREAL6:54

for b₁ being Point of (TOP-REAL 2)
for b₂ being Point of (Euclid 2)
for b₃ being non empty Subset of (TOP-REAL 2)
for b₄ being real number st b₃ = Ball b₂,b₄ & b₁ = b₂ holds
E-bound b₃ = (b₁ `1 ) + b₄

proof end;

theorem Th55: :: TOPREAL6:55

for b₁ being Point of (TOP-REAL 2)
for b₂ being Point of (Euclid 2)
for b₃ being non empty Subset of (TOP-REAL 2)
for b₄ being real number st b₃ = Ball b₂,b₄ & b₁ = b₂ holds
S-bound b₃ = (b₁ `2 ) - b₄

proof end;

theorem Th56: :: TOPREAL6:56

for b₁ being Point of (TOP-REAL 2)
for b₂ being Point of (Euclid 2)
for b₃ being non empty Subset of (TOP-REAL 2)
for b₄ being real number st b₃ = Ball b₂,b₄ & b₁ = b₂ holds
N-bound b₃ = (b₁ `2 ) + b₄

proof end;

theorem Th57: :: TOPREAL6:57

for b₁ being Point of (Euclid 2)
for b₂ being non empty Subset of (TOP-REAL 2)
for b₃ being real number st b₂ = Ball b₁,b₃ holds
not b₂ is horizontal

proof end;

theorem Th58: :: TOPREAL6:58

for b₁ being Point of (Euclid 2)
for b₂ being non empty Subset of (TOP-REAL 2)
for b₃ being real number st b₂ = Ball b₁,b₃ holds
not b₂ is vertical

proof end;

theorem Th59: :: TOPREAL6:59

for b₁ being Real
for b₂ being Point of (Euclid 2)
for b₃ being Point of (TOP-REAL 2) st b₃ in Ball b₂,b₁ holds
not |[((b₃ `1 ) - (2 * b₁)),(b₃ `2 )]| in Ball b₂,b₁

proof end;

theorem Th60: :: TOPREAL6:60

for b₁ being Real
for b₂ being non empty compact Subset of (TOP-REAL 2)
for b₃ being Point of (Euclid 2) st b₃ = 0.REAL 2 & b₁ > 0 holds
b₂ c= Ball b₃,(((((abs (E-bound b₂)) + (abs (N-bound b₂))) + (abs (W-bound b₂))) + (abs (S-bound b₂))) + b₁)

proof end;

theorem Th61: :: TOPREAL6:61

for b₁ being real number
for b₂ being non empty Reflexive symmetric triangle MetrStruct
for b₃ being Point of b₂ st b₁ < 0 holds
Sphere b₃,b₁ = {}

proof end;

theorem Th62: :: TOPREAL6:62

for b₁ being non empty Reflexive discerning MetrStruct
for b₂ being Point of b₁ holds Sphere b₂,0 = {b₂}

proof end;

theorem Th63: :: TOPREAL6:63

for b₁ being real number
for b₂ being non empty Reflexive symmetric triangle MetrStruct
for b₃ being Point of b₂ st b₁ < 0 holds
cl_Ball b₃,b₁ = {}

proof end;

theorem Th64: :: TOPREAL6:64

for b₁ being non empty MetrSpace
for b₂ being Point of b₁ holds cl_Ball b₂,0 = {b₂}

proof end;

Lemma30: for b₁ being non empty MetrSpace
for b₂ being Point of b₁
for b₃ being real number
for b₄ being Subset of (TopSpaceMetr b₁) st b₄ = cl_Ball b₂,b₃ holds
b₄ ` is open

proof end;

theorem Th65: :: TOPREAL6:65

for b₁ being non empty MetrSpace
for b₂ being Point of b₁
for b₃ being real number
for b₄ being Subset of (TopSpaceMetr b₁) st b₄ = cl_Ball b₂,b₃ holds
b₄ is closed

proof end;

theorem Th66: :: TOPREAL6:66

for b₁ being Nat
for b₂ being Point of (Euclid b₁)
for b₃ being Subset of (TOP-REAL b₁)
for b₄ being real number st b₃ = cl_Ball b₂,b₄ holds
b₃ is closed by Th65;

theorem Th67: :: TOPREAL6:67

for b₁ being non empty MetrSpace
for b₂ being Point of b₁
for b₃ being real number holds cl_Ball b₂,b₃ is bounded

proof end;

theorem Th68: :: TOPREAL6:68

for b₁ being non empty MetrSpace
for b₂ being Point of b₁
for b₃ being real number
for b₄ being Subset of (TopSpaceMetr b₁) st b₄ = Sphere b₂,b₃ holds
b₄ is closed

proof end;

theorem Th69: :: TOPREAL6:69

for b₁ being Nat
for b₂ being Point of (Euclid b₁)
for b₃ being Subset of (TOP-REAL b₁)
for b₄ being real number st b₃ = Sphere b₂,b₄ holds
b₃ is closed by Th68;

theorem Th70: :: TOPREAL6:70

for b₁ being non empty MetrSpace
for b₂ being Point of b₁
for b₃ being real number holds Sphere b₂,b₃ is bounded

proof end;

theorem Th71: :: TOPREAL6:71

for b₁ being Nat
for b₂ being Subset of (TOP-REAL b₁) st b₂ is Bounded holds
Cl b₂ is Bounded

proof end;

theorem Th72: :: TOPREAL6:72

for b₁ being non empty MetrStruct holds
( b₁ is bounded iff for b₂ being Subset of b₁ holds b₂ is bounded )

proof end;

theorem Th73: :: TOPREAL6:73

for b₁ being non empty Reflexive symmetric triangle MetrStruct
for b₂, b₃ being Subset of b₁ st the carrier of b₁ = b₂ \/ b₃ & not b₁ is bounded & b₂ is bounded holds
not b₃ is bounded

proof end;

theorem Th74: :: TOPREAL6:74

for b₁ being Nat
for b₂, b₃ being Subset of (TOP-REAL b₁) st b₁ >= 1 & the carrier of (TOP-REAL b₁) = b₂ \/ b₃ & b₂ is Bounded holds
not b₃ is Bounded

proof end;

theorem Th75: :: TOPREAL6:75

canceled;

theorem Th76: :: TOPREAL6:76

for b₁ being Nat
for b₂, b₃ being Subset of (TOP-REAL b₁) st b₂ is Bounded & b₃ is Bounded holds
b₂ \/ b₃ is Bounded

proof end;

registration

let c₁ be non empty Subset of REAL ;
cluster Cl a₁ -> non empty ;
coherence

proof end;

end;

registration

let c₁ be bounded_below Subset of REAL ;
cluster Cl a₁ -> bounded_below ;
coherence

proof end;

end;

registration

let c₁ be bounded_above Subset of REAL ;
cluster Cl a₁ -> bounded_above ;
coherence

proof end;

end;

theorem Th77: :: TOPREAL6:77

for b₁ being non empty bounded_below Subset of REAL holds inf b₁ = inf (Cl b₁)

proof end;

theorem Th78: :: TOPREAL6:78

for b₁ being non empty bounded_above Subset of REAL holds sup b₁ = sup (Cl b₁)

proof end;

registration

cluster R^1 -> being_T2 ;
coherence by PCOMPS_1:38, TOPMETR:def 7;

end;

Lemma39: R^1 = TopStruct(# the carrier of RealSpace ,(Family_open_set RealSpace ) #)
by PCOMPS_1:def 6, TOPMETR:def 7;

theorem Th79: :: TOPREAL6:79

for b₁ being Subset of REAL
for b₂ being Subset of R^1 st b₁ = b₂ holds
( b₁ is closed iff b₂ is closed )

proof end;

theorem Th80: :: TOPREAL6:80

for b₁ being Subset of REAL
for b₂ being Subset of R^1 st b₁ = b₂ holds
Cl b₁ = Cl b₂

proof end;

theorem Th81: :: TOPREAL6:81

for b₁ being Subset of REAL
for b₂ being Subset of R^1 st b₁ = b₂ holds
( b₁ is compact iff b₂ is compact )

proof end;

registration

cluster finite -> compact Element of bool REAL ;
coherence

proof end;

end;

registration

let c₁, c₂ be real number ;
cluster [.a₁,a₂.] -> compact ;
coherence by RCOMP_1:24;

end;

theorem Th82: :: TOPREAL6:82

for b₁, b₂ being real number holds
( b₁ <> b₂ iff Cl ].b₁,b₂.[ = [.b₁,b₂.] )

proof end;

registration

cluster non empty finite bounded compact Element of bool REAL ;
existence

proof end;

end;

theorem Th83: :: TOPREAL6:83

for b₁ being TopStruct
for b₂ being RealMap of b₁
for b₃ being Function of b₁,R^1 st b₂ = b₃ holds
( b₂ is continuous iff b₃ is continuous )

proof end;

theorem Th84: :: TOPREAL6:84

for b₁, b₂ being Subset of REAL
for b₃ being Function of [:R^1 ,R^1 :],(TOP-REAL 2) st ( for b₄, b₅ being Real holds b₃ . [b₄,b₅] = <*b₄,b₅*> ) holds
b₃ .: [:b₁,b₂:] = product (1,2 --> b₁,b₂)

proof end;

theorem Th85: :: TOPREAL6:85

for b₁ being Function of [:R^1 ,R^1 :],(TOP-REAL 2) st ( for b₂, b₃ being Real holds b₁ . [b₂,b₃] = <*b₂,b₃*> ) holds
b₁ is_homeomorphism

proof end;

theorem Th86: :: TOPREAL6:86

[:R^1 ,R^1 :], TOP-REAL 2 are_homeomorphic

proof end;

theorem Th87: :: TOPREAL6:87

for b₁, b₂ being compact Subset of REAL holds product (1,2 --> b₁,b₂) is compact Subset of (TOP-REAL 2)

proof end;

theorem Th88: :: TOPREAL6:88

for b₁ being Subset of (TOP-REAL 2) st b₁ is Bounded & b₁ is closed holds
b₁ is compact

proof end;

theorem Th89: :: TOPREAL6:89

for b₁ being Subset of (TOP-REAL 2) st b₁ is Bounded holds
for b₂ being continuous RealMap of (TOP-REAL 2) holds Cl (b₂ .: b₁) c= b₂ .: (Cl b₁)

proof end;

theorem Th90: :: TOPREAL6:90

for b₁ being Subset of (TOP-REAL 2) holds proj1 .: (Cl b₁) c= Cl (proj1 .: b₁)

proof end;

theorem Th91: :: TOPREAL6:91

for b₁ being Subset of (TOP-REAL 2) holds proj2 .: (Cl b₁) c= Cl (proj2 .: b₁)

proof end;

theorem Th92: :: TOPREAL6:92

for b₁ being Subset of (TOP-REAL 2) st b₁ is Bounded holds
Cl (proj1 .: b₁) = proj1 .: (Cl b₁)

proof end;

theorem Th93: :: TOPREAL6:93

for b₁ being Subset of (TOP-REAL 2) st b₁ is Bounded holds
Cl (proj2 .: b₁) = proj2 .: (Cl b₁)

proof end;

theorem Th94: :: TOPREAL6:94

for b₁ being non empty Subset of (TOP-REAL 2) st b₁ is Bounded holds
W-bound b₁ = W-bound (Cl b₁)

proof end;

theorem Th95: :: TOPREAL6:95

for b₁ being non empty Subset of (TOP-REAL 2) st b₁ is Bounded holds
E-bound b₁ = E-bound (Cl b₁)

proof end;

theorem Th96: :: TOPREAL6:96

for b₁ being non empty Subset of (TOP-REAL 2) st b₁ is Bounded holds
N-bound b₁ = N-bound (Cl b₁)

proof end;

theorem Th97: :: TOPREAL6:97

for b₁ being non empty Subset of (TOP-REAL 2) st b₁ is Bounded holds
S-bound b₁ = S-bound (Cl b₁)

proof end;