let s1, t1, s2, t2 be Real; :: thesis: for P, P1, P2 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 ) ) } & P1 = { pa where pa is Point of (TOP-REAL 2) : ( s1 < pa `1 & pa `1 < s2 & t1 < pa `2 & pa `2 < t2 ) } & P2 = { pb where pb is Point of (TOP-REAL 2) : ( not s1 <= pb `1 or not pb `1 <= s2 or not t1 <= pb `2 or not pb `2 <= t2 ) } holds
( P = (Cl P1) \ P1 & P = (Cl P2) \ P2 )
let P, P1, P2 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 ) ) } & P1 = { pa where pa is Point of (TOP-REAL 2) : ( s1 < pa `1 & pa `1 < s2 & t1 < pa `2 & pa `2 < t2 ) } & P2 = { pb where pb is Point of (TOP-REAL 2) : ( not s1 <= pb `1 or not pb `1 <= s2 or not t1 <= pb `2 or not pb `2 <= t2 ) } implies ( P = (Cl P1) \ P1 & P = (Cl P2) \ P2 ) )
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 ) ) } and
A4: P1 = { pa where pa is Point of (TOP-REAL 2) : ( s1 < pa `1 & pa `1 < s2 & t1 < pa `2 & pa `2 < t2 ) } and
A5: P2 = { pb where pb is Point of (TOP-REAL 2) : ( not s1 <= pb `1 or not pb `1 <= s2 or not t1 <= pb `2 or not pb `2 <= t2 ) } ; :: thesis: ( P = (Cl P1) \ P1 & P = (Cl P2) \ P2 )
reconsider PP = P ` as Subset of (TOP-REAL 2) ;
PP = P1 \/ P2 by A1, A2, A3, A4, A5, Th30;
then P = (P1 \/ P2) ` ;
then A6: P = (([#] (TOP-REAL 2)) \ P1) /\ (([#] (TOP-REAL 2)) \ P2) by XBOOLE_1:53;
then A7: P c= ([#] (TOP-REAL 2)) \ P2 by XBOOLE_1:17;
A8: Cl P2 = P \/ P2 by A1, A2, A3, A5, Lm11;
A9: (P \/ P2) \ P2 c= P
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (P \/ P2) \ P2 or x in P )
assume A10: x in (P \/ P2) \ P2 ; :: thesis: x in P
then A11: x in P \/ P2 by XBOOLE_0:def 5;
not x in P2 by A10, XBOOLE_0:def 5;
hence x in P by A11, XBOOLE_0:def 3; :: thesis: verum
end;
P c= Cl P2 by A8, XBOOLE_1:7;
then P c= (Cl P2) /\ (P2 `) by A7, XBOOLE_1:19;
then A12: P c= (Cl P2) \ P2 by SUBSET_1:13;
A13: P c= ([#] (TOP-REAL 2)) \ P1 by A6, XBOOLE_1:17;
A14: Cl P1 = P \/ P1 by A1, A2, A3, A4, Lm10;
A15: (P \/ P1) \ P1 c= P
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (P \/ P1) \ P1 or x in P )
assume A16: x in (P \/ P1) \ P1 ; :: thesis: x in P
then A17: x in P \/ P1 by XBOOLE_0:def 5;
not x in P1 by A16, XBOOLE_0:def 5;
hence x in P by A17, XBOOLE_0:def 3; :: thesis: verum
end;
P c= Cl P1 by A14, XBOOLE_1:7;
then P c= (Cl P1) /\ (P1 `) by A13, XBOOLE_1:19;
then P c= (Cl P1) \ P1 by SUBSET_1:13;
hence ( P = (Cl P1) \ P1 & P = (Cl P2) \ P2 ) by A8, A9, A12, A14, A15; :: thesis: verum