let s1, s2, t1, t2 be Real; :: thesis: for P being Subset of (TOP-REAL 2) st s1 < s2 & t1 < t2 & P = { p where p is Point of (TOP-REAL 2) : ( ( p `1 = s1 & p `2 <= t2 & p `2 >= t1 ) or ( p `1 <= s2 & p `1 >= s1 & p `2 = t2 ) or ( p `1 <= s2 & p `1 >= s1 & p `2 = t1 ) or ( p `1 = s2 & p `2 <= t2 & p `2 >= t1 ) ) } holds
P is Jordan
let P be Subset of (TOP-REAL 2); :: thesis: ( s1 < s2 & t1 < t2 & P = { p where p is Point of (TOP-REAL 2) : ( ( p `1 = s1 & p `2 <= t2 & p `2 >= t1 ) or ( p `1 <= s2 & p `1 >= s1 & p `2 = t2 ) or ( p `1 <= s2 & p `1 >= s1 & p `2 = t1 ) or ( p `1 = s2 & p `2 <= t2 & p `2 >= t1 ) ) } implies P is Jordan )
assume that
A1: s1 < s2 and
A2: t1 < t2 and
A3: P = { p where p is Point of (TOP-REAL 2) : ( ( p `1 = s1 & p `2 <= t2 & p `2 >= t1 ) or ( p `1 <= s2 & p `1 >= s1 & p `2 = t2 ) or ( p `1 <= s2 & p `1 >= s1 & p `2 = t1 ) or ( p `1 = s2 & p `2 <= t2 & p `2 >= t1 ) ) } ; :: thesis: P is Jordan
reconsider P1 = { pa where pa is Point of (TOP-REAL 2) : ( s1 < pa `1 & pa `1 < s2 & t1 < pa `2 & pa `2 < t2 ) } , P2 = { pc where pc is Point of (TOP-REAL 2) : ( not s1 <= pc `1 or not pc `1 <= s2 or not t1 <= pc `2 or not pc `2 <= t2 ) } as Subset of (TOP-REAL 2) by Th23, Th24;
reconsider PC = P ` as Subset of (TOP-REAL 2) ;
A4: P1 = { pa where pa is Point of (TOP-REAL 2) : ( s1 < pa `1 & pa `1 < s2 & t1 < pa `2 & pa `2 < t2 ) } ;
A5: P2 = { pc where pc is Point of (TOP-REAL 2) : ( not s1 <= pc `1 or not pc `1 <= s2 or not t1 <= pc `2 or not pc `2 <= t2 ) } ;
A6: PC = P1 \/ P2 by A1, A2, A3, Th30;
A7: PC <> {} by A1, A2, A3, A4, A5, Th30;
A8: P1 misses P2 by A1, A2, A3, Th30;
A9: P = (Cl P1) \ P1 by A1, A2, A3, A5, Th31;
A10: P = (Cl P2) \ P2 by A1, A2, A3, A4, Th31;
for P1A, P2B being Subset of ((TOP-REAL 2) | (P `)) st P1A = P1 & P2B = P2 holds
( P1A is a_component & P2B is a_component ) by A1, A2, A3, Th30;
hence P is Jordan by A6, A7, A8, A9, A10; :: thesis: verum