:: TOPMETR2 semantic presentation

theorem Th1: :: TOPMETR2:1

for b₁, b₂, b₃ being real number st b₁ <= b₂ & b₂ <= b₃ holds
[.b₁,b₂.] /\ [.b₂,b₃.] = {b₂}

proof end;

theorem Th2: :: TOPMETR2:2

for b₁, b₂ being Function st b₁ is one-to-one & b₂ is one-to-one & ( for b₃, b₄ being set st b₃ in dom b₂ & b₄ in (dom b₁) \ (dom b₂) holds
b₂ . b₃ <> b₁ . b₄ ) holds
b₁ +* b₂ is one-to-one

proof end;

Lemma2: for b₁, b₂ being Function st b₁ .: ((dom b₁) /\ (dom b₂)) c= rng b₂ holds
(rng b₁) \ (rng b₂) c= rng (b₁ +* b₂)

proof end;

theorem Th3: :: TOPMETR2:3

for b₁, b₂ being Function st b₁ .: ((dom b₁) /\ (dom b₂)) c= rng b₂ holds
(rng b₁) \/ (rng b₂) = rng (b₁ +* b₂)

proof end;

theorem Th4: :: TOPMETR2:4

for b₁, b₂ being non empty TopSpace
for b₃ being Point of b₁
for b₄, b₅ being SubSpace of b₁
for b₆ being Function of b₄,b₂
for b₇ being Function of b₅,b₂ st ([#] b₄) \/ ([#] b₅) = [#] b₁ & ([#] b₄) /\ ([#] b₅) = {b₃} & b₄ is compact & b₅ is compact & b₁ is_T2 & b₆ is continuous & b₇ is continuous & b₆ . b₃ = b₇ . b₃ holds
b₆ +* b₇ is continuous Function of b₁,b₂

proof end;

theorem Th5: :: TOPMETR2:5

for b₁, b₂ being non empty TopSpace
for b₃, b₄ being SubSpace of b₂
for b₅, b₆ being Point of b₂
for b₇ being Function of b₃,b₁
for b₈ being Function of b₄,b₁ st ([#] b₃) \/ ([#] b₄) = [#] b₂ & ([#] b₃) /\ ([#] b₄) = {b₅,b₆} & b₃ is compact & b₄ is compact & b₂ is_T2 & b₇ is continuous & b₈ is continuous & b₇ . b₅ = b₈ . b₅ & b₇ . b₆ = b₈ . b₆ holds
b₇ +* b₈ is continuous Function of b₂,b₁

proof end;

theorem Th6: :: TOPMETR2:6

for b₁ being being_T2 TopSpace
for b₂, b₃ being Subset of b₁
for b₄ being Point of b₁
for b₅ being Function of I[01] ,(b₁ | b₂)
for b₆ being Function of I[01] ,(b₁ | b₃) st b₂ /\ b₃ = {b₄} & b₅ is_homeomorphism & b₅ . 1 = b₄ & b₆ is_homeomorphism & b₆ . 0 = b₄ holds
ex b₇ being Function of I[01] ,(b₁ | (b₂ \/ b₃)) st
( b₇ is_homeomorphism & b₇ . 0 = b₅ . 0 & b₇ . 1 = b₆ . 1 )

proof end;