:: JORDAN1 semantic presentation

theorem Th1: :: JORDAN1:1
for b1 being TopStruct
for b2 being Subset of b1 holds the carrier of (b1 | b2) = b2
proof end;

theorem Th2: :: JORDAN1:2
for b1 being non empty TopSpace st ( for b2, b3 being Point of b1 ex b4 being non empty TopSpace st
( b4 is connected & ex b5 being Function of b4,b1 st
( b5 is continuous & b2 in rng b5 & b3 in rng b5 ) ) ) holds
b1 is connected
proof end;

Lemma3: ( 0 in [.0,1.] & 1 in [.0,1.] )
proof end;

theorem Th3: :: JORDAN1:3
canceled;

theorem Th4: :: JORDAN1:4
for b1 being non empty TopSpace st ( for b2, b3 being Point of b1 ex b4 being Function of I[01] ,b1 st
( b4 is continuous & b2 = b4 . 0 & b3 = b4 . 1 ) ) holds
b1 is connected
proof end;

theorem Th5: :: JORDAN1:5
for b1 being non empty TopSpace
for b2 being Subset of b1 st ( for b3, b4 being Point of b1 st b3 in b2 & b4 in b2 & b3 <> b4 holds
ex b5 being Function of I[01] ,(b1 | b2) st
( b5 is continuous & b3 = b5 . 0 & b4 = b5 . 1 ) ) holds
b2 is connected
proof end;

theorem Th6: :: JORDAN1:6
for b1 being non empty TopSpace
for b2, b3 being Subset of b1 st b2 is connected & b3 is connected & b2 meets b3 holds
b2 \/ b3 is connected
proof end;

theorem Th7: :: JORDAN1:7
for b1 being non empty TopSpace
for b2, b3, b4 being Subset of b1 st b2 is connected & b3 is connected & b4 is connected & b2 meets b3 & b3 meets b4 holds
(b2 \/ b3) \/ b4 is connected
proof end;

theorem Th8: :: JORDAN1:8
for b1 being non empty TopSpace
for b2, b3, b4, b5 being Subset of b1 st b2 is connected & b3 is connected & b4 is connected & b5 is connected & b2 meets b3 & b3 meets b4 & b4 meets b5 holds
((b2 \/ b3) \/ b4) \/ b5 is connected
proof end;

definition
let c1 be Nat;
let c2 be Subset of (TOP-REAL c1);
attr a2 is convex means :: JORDAN1:def 1
for b1, b2 being Point of (TOP-REAL a1) st b1 in a2 & b2 in a2 holds
LSeg b1,b2 c= a2;
end;

:: deftheorem Def1 defines convex JORDAN1:def 1 :
for b1 being Nat
for b2 being Subset of (TOP-REAL b1) holds
( b2 is convex iff for b3, b4 being Point of (TOP-REAL b1) st b3 in b2 & b4 in b2 holds
LSeg b3,b4 c= b2 );

theorem Th9: :: JORDAN1:9
for b1 being Nat
for b2 being Subset of (TOP-REAL b1) st b2 is convex holds
b2 is connected
proof end;

Lemma10: the carrier of (TOP-REAL 2) = REAL 2
by EUCLID:25;

Lemma11: for b1 being Real holds { |[b2,b3]| where B is Real, B is Real : b2 < b1 } is Subset of (REAL 2)
proof end;

Lemma12: for b1 being Real holds { |[b2,b3]| where B is Real, B is Real : b3 < b1 } is Subset of (REAL 2)
proof end;

Lemma13: for b1 being Real holds { |[b2,b3]| where B is Real, B is Real : b1 < b2 } is Subset of (REAL 2)
proof end;

Lemma14: for b1 being Real holds { |[b2,b3]| where B is Real, B is Real : b1 < b3 } is Subset of (REAL 2)
proof end;

Lemma15: for b1, b2, b3, b4 being Real holds { |[b5,b6]| where B is Real, B is Real : ( b1 < b5 & b5 < b2 & b3 < b6 & b6 < b4 ) } is Subset of (REAL 2)
proof end;

Lemma16: for b1, b2, b3, b4 being Real holds { |[b5,b6]| where B is Real, B is Real : ( not b1 <= b5 or not b5 <= b2 or not b3 <= b6 or not b6 <= b4 ) } is Subset of (REAL 2)
proof end;

theorem Th10: :: JORDAN1:10
canceled;

theorem Th11: :: JORDAN1:11
canceled;

theorem Th12: :: JORDAN1:12
for b1, b2, b3, b4 being Real holds { |[b5,b6]| where B is Real, B is Real : ( b1 < b5 & b5 < b2 & b3 < b6 & b6 < b4 ) } = (({ |[b5,b6]| where B is Real, B is Real : b1 < b5 } /\ { |[b5,b6]| where B is Real, B is Real : b5 < b2 } ) /\ { |[b5,b6]| where B is Real, B is Real : b3 < b6 } ) /\ { |[b5,b6]| where B is Real, B is Real : b6 < b4 }
proof end;

theorem Th13: :: JORDAN1:13
for b1, b2, b3, b4 being Real holds { |[b5,b6]| where B is Real, B is Real : ( not b1 <= b5 or not b5 <= b2 or not b3 <= b6 or not b6 <= b4 ) } = (({ |[b5,b6]| where B is Real, B is Real : b5 < b1 } \/ { |[b5,b6]| where B is Real, B is Real : b6 < b3 } ) \/ { |[b5,b6]| where B is Real, B is Real : b2 < b5 } ) \/ { |[b5,b6]| where B is Real, B is Real : b4 < b6 }
proof end;

theorem Th14: :: JORDAN1:14
for b1, b2, b3, b4 being Real
for b5 being Subset of (TOP-REAL 2) st b5 = { |[b6,b7]| where B is Real, B is Real : ( b1 < b6 & b6 < b3 & b2 < b7 & b7 < b4 ) } holds
b5 is convex
proof end;

theorem Th15: :: JORDAN1:15
for b1, b2, b3, b4 being Real
for b5 being Subset of (TOP-REAL 2) st b5 = { |[b6,b7]| where B is Real, B is Real : ( b1 < b6 & b6 < b3 & b2 < b7 & b7 < b4 ) } holds
b5 is connected
proof end;

theorem Th16: :: JORDAN1:16
for b1 being Real
for b2 being Subset of (TOP-REAL 2) st b2 = { |[b3,b4]| where B is Real, B is Real : b1 < b3 } holds
b2 is convex
proof end;

theorem Th17: :: JORDAN1:17
for b1 being Real
for b2 being Subset of (TOP-REAL 2) st b2 = { |[b3,b4]| where B is Real, B is Real : b1 < b3 } holds
b2 is connected
proof end;

theorem Th18: :: JORDAN1:18
for b1 being Real
for b2 being Subset of (TOP-REAL 2) st b2 = { |[b3,b4]| where B is Real, B is Real : b3 < b1 } holds
b2 is convex
proof end;

theorem Th19: :: JORDAN1:19
for b1 being Real
for b2 being Subset of (TOP-REAL 2) st b2 = { |[b3,b4]| where B is Real, B is Real : b3 < b1 } holds
b2 is connected
proof end;

theorem Th20: :: JORDAN1:20
for b1 being Real
for b2 being Subset of (TOP-REAL 2) st b2 = { |[b3,b4]| where B is Real, B is Real : b1 < b4 } holds
b2 is convex
proof end;

theorem Th21: :: JORDAN1:21
for b1 being Real
for b2 being Subset of (TOP-REAL 2) st b2 = { |[b3,b4]| where B is Real, B is Real : b1 < b4 } holds
b2 is connected
proof end;

theorem Th22: :: JORDAN1:22
for b1 being Real
for b2 being Subset of (TOP-REAL 2) st b2 = { |[b3,b4]| where B is Real, B is Real : b4 < b1 } holds
b2 is convex
proof end;

theorem Th23: :: JORDAN1:23
for b1 being Real
for b2 being Subset of (TOP-REAL 2) st b2 = { |[b3,b4]| where B is Real, B is Real : b4 < b1 } holds
b2 is connected
proof end;

theorem Th24: :: JORDAN1:24
for b1, b2, b3, b4 being Real
for b5 being Subset of (TOP-REAL 2) st b5 = { |[b6,b7]| where B is Real, B is Real : ( not b1 <= b6 or not b6 <= b3 or not b2 <= b7 or not b7 <= b4 ) } holds
b5 is connected
proof end;

Lemma30: for b1, b2 being Real holds (b2 - b1) ^2 = (b1 - b2) ^2
proof end;

Lemma31: TOP-REAL 2 = TopSpaceMetr (Euclid 2)
by EUCLID:def 8;

theorem Th25: :: JORDAN1:25
for b1 being Real
for b2 being Subset of (TOP-REAL 2) st b2 = { |[b3,b4]| where B is Real, B is Real : b1 < b3 } holds
b2 is open
proof end;

theorem Th26: :: JORDAN1:26
for b1 being Real
for b2 being Subset of (TOP-REAL 2) st b2 = { |[b3,b4]| where B is Real, B is Real : b1 > b3 } holds
b2 is open
proof end;

theorem Th27: :: JORDAN1:27
for b1 being Real
for b2 being Subset of (TOP-REAL 2) st b2 = { |[b3,b4]| where B is Real, B is Real : b1 < b4 } holds
b2 is open
proof end;

theorem Th28: :: JORDAN1:28
for b1 being Real
for b2 being Subset of (TOP-REAL 2) st b2 = { |[b3,b4]| where B is Real, B is Real : b1 > b4 } holds
b2 is open
proof end;

theorem Th29: :: JORDAN1:29
for b1, b2, b3, b4 being Real
for b5 being Subset of (TOP-REAL 2) st b5 = { |[b6,b7]| where B is Real, B is Real : ( b1 < b6 & b6 < b3 & b2 < b7 & b7 < b4 ) } holds
b5 is open
proof end;

theorem Th30: :: JORDAN1:30
for b1, b2, b3, b4 being Real
for b5 being Subset of (TOP-REAL 2) st b5 = { |[b6,b7]| where B is Real, B is Real : ( not b1 <= b6 or not b6 <= b3 or not b2 <= b7 or not b7 <= b4 ) } holds
b5 is open
proof end;

theorem Th31: :: JORDAN1:31
for b1, b2, b3, b4 being Real
for b5, b6 being Subset of (TOP-REAL 2) st b5 = { |[b7,b8]| where B is Real, B is Real : ( b1 < b7 & b7 < b3 & b2 < b8 & b8 < b4 ) } & b6 = { |[b7,b8]| where B is Real, B is Real : ( not b1 <= b7 or not b7 <= b3 or not b2 <= b8 or not b8 <= b4 ) } holds
b5 misses b6
proof end;

theorem Th32: :: JORDAN1:32
for b1, b2, b3, b4 being Real holds { b5 where B is Point of (TOP-REAL 2) : ( b1 < b5 `1 & b5 `1 < b2 & b3 < b5 `2 & b5 `2 < b4 ) } = { |[b5,b6]| where B is Real, B is Real : ( b1 < b5 & b5 < b2 & b3 < b6 & b6 < b4 ) }
proof end;

theorem Th33: :: JORDAN1:33
for b1, b2, b3, b4 being Real holds { b5 where B is Point of (TOP-REAL 2) : ( not b1 <= b5 `1 or not b5 `1 <= b2 or not b3 <= b5 `2 or not b5 `2 <= b4 ) } = { |[b5,b6]| where B is Real, B is Real : ( not b1 <= b5 or not b5 <= b2 or not b3 <= b6 or not b6 <= b4 ) }
proof end;

theorem Th34: :: JORDAN1:34
for b1, b2, b3, b4 being Real holds { b5 where B is Point of (TOP-REAL 2) : ( b1 < b5 `1 & b5 `1 < b2 & b3 < b5 `2 & b5 `2 < b4 ) } is Subset of (TOP-REAL 2)
proof end;

theorem Th35: :: JORDAN1:35
for b1, b2, b3, b4 being Real holds { b5 where B is Point of (TOP-REAL 2) : ( not b1 <= b5 `1 or not b5 `1 <= b2 or not b3 <= b5 `2 or not b5 `2 <= b4 ) } is Subset of (TOP-REAL 2)
proof end;

theorem Th36: :: JORDAN1:36
for b1, b2, b3, b4 being Real
for b5 being Subset of (TOP-REAL 2) st b5 = { b6 where B is Point of (TOP-REAL 2) : ( b1 < b6 `1 & b6 `1 < b3 & b2 < b6 `2 & b6 `2 < b4 ) } holds
b5 is connected
proof end;

theorem Th37: :: JORDAN1:37
for b1, b2, b3, b4 being Real
for b5 being Subset of (TOP-REAL 2) st b5 = { b6 where B is Point of (TOP-REAL 2) : ( not b1 <= b6 `1 or not b6 `1 <= b3 or not b2 <= b6 `2 or not b6 `2 <= b4 ) } holds
b5 is connected
proof end;

theorem Th38: :: JORDAN1:38
for b1, b2, b3, b4 being Real
for b5 being Subset of (TOP-REAL 2) st b5 = { b6 where B is Point of (TOP-REAL 2) : ( b1 < b6 `1 & b6 `1 < b3 & b2 < b6 `2 & b6 `2 < b4 ) } holds
b5 is open
proof end;

theorem Th39: :: JORDAN1:39
for b1, b2, b3, b4 being Real
for b5 being Subset of (TOP-REAL 2) st b5 = { b6 where B is Point of (TOP-REAL 2) : ( not b1 <= b6 `1 or not b6 `1 <= b3 or not b2 <= b6 `2 or not b6 `2 <= b4 ) } holds
b5 is open
proof end;

theorem Th40: :: JORDAN1:40
for b1, b2, b3, b4 being Real
for b5, b6 being Subset of (TOP-REAL 2) st b5 = { b7 where B is Point of (TOP-REAL 2) : ( b1 < b7 `1 & b7 `1 < b3 & b2 < b7 `2 & b7 `2 < b4 ) } & b6 = { b7 where B is Point of (TOP-REAL 2) : ( not b1 <= b7 `1 or not b7 `1 <= b3 or not b2 <= b7 `2 or not b7 `2 <= b4 ) } holds
b5 misses b6
proof end;

theorem Th41: :: JORDAN1:41
for b1, b2, b3, b4 being Real
for b5, b6, b7 being Subset of (TOP-REAL 2) st b1 < b3 & b2 < b4 & b5 = { b8 where B is Point of (TOP-REAL 2) : ( ( b8 `1 = b1 & b8 `2 <= b4 & b8 `2 >= b2 ) or ( b8 `1 <= b3 & b8 `1 >= b1 & b8 `2 = b4 ) or ( b8 `1 <= b3 & b8 `1 >= b1 & b8 `2 = b2 ) or ( b8 `1 = b3 & b8 `2 <= b4 & b8 `2 >= b2 ) ) } & b6 = { b8 where B is Point of (TOP-REAL 2) : ( b1 < b8 `1 & b8 `1 < b3 & b2 < b8 `2 & b8 `2 < b4 ) } & b7 = { b8 where B is Point of (TOP-REAL 2) : ( not b1 <= b8 `1 or not b8 `1 <= b3 or not b2 <= b8 `2 or not b8 `2 <= b4 ) } holds
( b5 ` = b6 \/ b7 & b5 ` <> {} & b6 misses b7 & ( for b8, b9 being Subset of ((TOP-REAL 2) | (b5 ` )) st b8 = b6 & b9 = b7 holds
( b8 is_a_component_of (TOP-REAL 2) | (b5 ` ) & b9 is_a_component_of (TOP-REAL 2) | (b5 ` ) ) ) )
proof end;

Lemma49: for b1, b2, b3, b4 being Real
for b5, b6 being Subset of (TOP-REAL 2) st b1 < b3 & b2 < b4 & b5 = { b7 where B is Point of (TOP-REAL 2) : ( ( b7 `1 = b1 & b7 `2 <= b4 & b7 `2 >= b2 ) or ( b7 `1 <= b3 & b7 `1 >= b1 & b7 `2 = b4 ) or ( b7 `1 <= b3 & b7 `1 >= b1 & b7 `2 = b2 ) or ( b7 `1 = b3 & b7 `2 <= b4 & b7 `2 >= b2 ) ) } & b6 = { b7 where B is Point of (TOP-REAL 2) : ( b1 < b7 `1 & b7 `1 < b3 & b2 < b7 `2 & b7 `2 < b4 ) } holds
Cl b6 = b5 \/ b6
proof end;

Lemma50: for b1, b2, b3, b4 being Real
for b5, b6 being Subset of (TOP-REAL 2) st b1 < b3 & b2 < b4 & b5 = { b7 where B is Point of (TOP-REAL 2) : ( ( b7 `1 = b1 & b7 `2 <= b4 & b7 `2 >= b2 ) or ( b7 `1 <= b3 & b7 `1 >= b1 & b7 `2 = b4 ) or ( b7 `1 <= b3 & b7 `1 >= b1 & b7 `2 = b2 ) or ( b7 `1 = b3 & b7 `2 <= b4 & b7 `2 >= b2 ) ) } & b6 = { b7 where B is Point of (TOP-REAL 2) : ( not b1 <= b7 `1 or not b7 `1 <= b3 or not b2 <= b7 `2 or not b7 `2 <= b4 ) } holds
Cl b6 = b5 \/ b6
proof end;

theorem Th42: :: JORDAN1:42
for b1, b2, b3, b4 being Real
for b5, b6, b7 being Subset of (TOP-REAL 2) st b1 < b3 & b2 < b4 & b5 = { b8 where B is Point of (TOP-REAL 2) : ( ( b8 `1 = b1 & b8 `2 <= b4 & b8 `2 >= b2 ) or ( b8 `1 <= b3 & b8 `1 >= b1 & b8 `2 = b4 ) or ( b8 `1 <= b3 & b8 `1 >= b1 & b8 `2 = b2 ) or ( b8 `1 = b3 & b8 `2 <= b4 & b8 `2 >= b2 ) ) } & b6 = { b8 where B is Point of (TOP-REAL 2) : ( b1 < b8 `1 & b8 `1 < b3 & b2 < b8 `2 & b8 `2 < b4 ) } & b7 = { b8 where B is Point of (TOP-REAL 2) : ( not b1 <= b8 `1 or not b8 `1 <= b3 or not b2 <= b8 `2 or not b8 `2 <= b4 ) } holds
( b5 = (Cl b6) \ b6 & b5 = (Cl b7) \ b7 )
proof end;

theorem Th43: :: JORDAN1:43
for b1, b2, b3, b4 being Real
for b5, b6 being Subset of (TOP-REAL 2) st b5 = { b7 where B is Point of (TOP-REAL 2) : ( ( b7 `1 = b1 & b7 `2 <= b4 & b7 `2 >= b3 ) or ( b7 `1 <= b2 & b7 `1 >= b1 & b7 `2 = b4 ) or ( b7 `1 <= b2 & b7 `1 >= b1 & b7 `2 = b3 ) or ( b7 `1 = b2 & b7 `2 <= b4 & b7 `2 >= b3 ) ) } & b6 = { b7 where B is Point of (TOP-REAL 2) : ( b1 < b7 `1 & b7 `1 < b2 & b3 < b7 `2 & b7 `2 < b4 ) } holds
b6 c= [#] ((TOP-REAL 2) | (b5 ` ))
proof end;

theorem Th44: :: JORDAN1:44
for b1, b2, b3, b4 being Real
for b5, b6 being Subset of (TOP-REAL 2) st b5 = { b7 where B is Point of (TOP-REAL 2) : ( ( b7 `1 = b1 & b7 `2 <= b4 & b7 `2 >= b3 ) or ( b7 `1 <= b2 & b7 `1 >= b1 & b7 `2 = b4 ) or ( b7 `1 <= b2 & b7 `1 >= b1 & b7 `2 = b3 ) or ( b7 `1 = b2 & b7 `2 <= b4 & b7 `2 >= b3 ) ) } & b6 = { b7 where B is Point of (TOP-REAL 2) : ( b1 < b7 `1 & b7 `1 < b2 & b3 < b7 `2 & b7 `2 < b4 ) } holds
b6 is Subset of ((TOP-REAL 2) | (b5 ` ))
proof end;

theorem Th45: :: JORDAN1:45
for b1, b2, b3, b4 being Real
for b5, b6 being Subset of (TOP-REAL 2) st b1 < b2 & b3 < b4 & b5 = { b7 where B is Point of (TOP-REAL 2) : ( ( b7 `1 = b1 & b7 `2 <= b4 & b7 `2 >= b3 ) or ( b7 `1 <= b2 & b7 `1 >= b1 & b7 `2 = b4 ) or ( b7 `1 <= b2 & b7 `1 >= b1 & b7 `2 = b3 ) or ( b7 `1 = b2 & b7 `2 <= b4 & b7 `2 >= b3 ) ) } & b6 = { b7 where B is Point of (TOP-REAL 2) : ( not b1 <= b7 `1 or not b7 `1 <= b2 or not b3 <= b7 `2 or not b7 `2 <= b4 ) } holds
b6 c= [#] ((TOP-REAL 2) | (b5 ` ))
proof end;

theorem Th46: :: JORDAN1:46
for b1, b2, b3, b4 being Real
for b5, b6 being Subset of (TOP-REAL 2) st b1 < b2 & b3 < b4 & b5 = { b7 where B is Point of (TOP-REAL 2) : ( ( b7 `1 = b1 & b7 `2 <= b4 & b7 `2 >= b3 ) or ( b7 `1 <= b2 & b7 `1 >= b1 & b7 `2 = b4 ) or ( b7 `1 <= b2 & b7 `1 >= b1 & b7 `2 = b3 ) or ( b7 `1 = b2 & b7 `2 <= b4 & b7 `2 >= b3 ) ) } & b6 = { b7 where B is Point of (TOP-REAL 2) : ( not b1 <= b7 `1 or not b7 `1 <= b2 or not b3 <= b7 `2 or not b7 `2 <= b4 ) } holds
b6 is Subset of ((TOP-REAL 2) | (b5 ` ))
proof end;

definition
let c1 be Subset of (TOP-REAL 2);
attr a1 is Jordan means :Def2: :: JORDAN1:def 2
( a1 ` <> {} & ex b1, b2 being Subset of (TOP-REAL 2) st
( a1 ` = b1 \/ b2 & b1 misses b2 & (Cl b1) \ b1 = (Cl b2) \ b2 & ( for b3, b4 being Subset of ((TOP-REAL 2) | (a1 ` )) st b3 = b1 & b4 = b2 holds
( b3 is_a_component_of (TOP-REAL 2) | (a1 ` ) & b4 is_a_component_of (TOP-REAL 2) | (a1 ` ) ) ) ) );
end;

:: deftheorem Def2 defines Jordan JORDAN1:def 2 :
for b1 being Subset of (TOP-REAL 2) holds
( b1 is Jordan iff ( b1 ` <> {} & ex b2, b3 being Subset of (TOP-REAL 2) st
( b1 ` = b2 \/ b3 & b2 misses b3 & (Cl b2) \ b2 = (Cl b3) \ b3 & ( for b4, b5 being Subset of ((TOP-REAL 2) | (b1 ` )) st b4 = b2 & b5 = b3 holds
( b4 is_a_component_of (TOP-REAL 2) | (b1 ` ) & b5 is_a_component_of (TOP-REAL 2) | (b1 ` ) ) ) ) ) );

notation
let c1 be Subset of (TOP-REAL 2);
synonym c1 has_property_J for Jordan c1;
end;

theorem Th47: :: JORDAN1:47
for b1 being Subset of (TOP-REAL 2) st b1 has_property_J holds
( b1 ` <> {} & ex b2, b3 being Subset of (TOP-REAL 2)ex b4, b5 being Subset of ((TOP-REAL 2) | (b1 ` )) st
( b1 ` = b2 \/ b3 & b2 misses b3 & (Cl b2) \ b2 = (Cl b3) \ b3 & b4 = b2 & b5 = b3 & b4 is_a_component_of (TOP-REAL 2) | (b1 ` ) & b5 is_a_component_of (TOP-REAL 2) | (b1 ` ) & ( for b6 being Subset of ((TOP-REAL 2) | (b1 ` )) holds
( not b6 is_a_component_of (TOP-REAL 2) | (b1 ` ) or b6 = b4 or b6 = b5 ) ) ) )
proof end;

theorem Th48: :: JORDAN1:48
for b1, b2, b3, b4 being Real
for b5 being Subset of (TOP-REAL 2) st b1 < b2 & b3 < b4 & b5 = { b6 where B is Point of (TOP-REAL 2) : ( ( b6 `1 = b1 & b6 `2 <= b4 & b6 `2 >= b3 ) or ( b6 `1 <= b2 & b6 `1 >= b1 & b6 `2 = b4 ) or ( b6 `1 <= b2 & b6 `1 >= b1 & b6 `2 = b3 ) or ( b6 `1 = b2 & b6 `2 <= b4 & b6 `2 >= b3 ) ) } holds
b5 has_property_J
proof end;

theorem Th49: :: JORDAN1:49
for b1, b2, b3, b4 being Real
for b5, b6 being Subset of (TOP-REAL 2) st b1 < b3 & b2 < b4 & b5 = { b7 where B is Point of (TOP-REAL 2) : ( ( b7 `1 = b1 & b7 `2 <= b4 & b7 `2 >= b2 ) or ( b7 `1 <= b3 & b7 `1 >= b1 & b7 `2 = b4 ) or ( b7 `1 <= b3 & b7 `1 >= b1 & b7 `2 = b2 ) or ( b7 `1 = b3 & b7 `2 <= b4 & b7 `2 >= b2 ) ) } & b6 = { b7 where B is Point of (TOP-REAL 2) : ( not b1 <= b7 `1 or not b7 `1 <= b3 or not b2 <= b7 `2 or not b7 `2 <= b4 ) } holds
Cl b6 = b5 \/ b6 by Lemma50;

theorem Th50: :: JORDAN1:50
for b1, b2, b3, b4 being Real
for b5, b6 being Subset of (TOP-REAL 2) st b1 < b3 & b2 < b4 & b5 = { b7 where B is Point of (TOP-REAL 2) : ( ( b7 `1 = b1 & b7 `2 <= b4 & b7 `2 >= b2 ) or ( b7 `1 <= b3 & b7 `1 >= b1 & b7 `2 = b4 ) or ( b7 `1 <= b3 & b7 `1 >= b1 & b7 `2 = b2 ) or ( b7 `1 = b3 & b7 `2 <= b4 & b7 `2 >= b2 ) ) } & b6 = { b7 where B is Point of (TOP-REAL 2) : ( b1 < b7 `1 & b7 `1 < b3 & b2 < b7 `2 & b7 `2 < b4 ) } holds
Cl b6 = b5 \/ b6 by Lemma49;