let s1, t1, s2, t2 be Real; 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); ( 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 ) }
; ( 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
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
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; verum