let S be TopSpace; :: thesis: for P1, P2 being Subset of S
for P1' being Subset of (S | P2) st P1 = P1' & P1 c= P2 holds
S | P1 = (S | P2) | P1'
let P1, P2 be Subset of S; :: thesis: for P1' being Subset of (S | P2) st P1 = P1' & P1 c= P2 holds
S | P1 = (S | P2) | P1'
let P1' be Subset of (S | P2); :: thesis: ( P1 = P1' & P1 c= P2 implies S | P1 = (S | P2) | P1' )
assume A1: ( P1 = P1' & P1 c= P2 ) ; :: thesis: S | P1 = (S | P2) | P1'
A2: [#] (S | P2) = P2 by Def10;
A3: [#] ((S | P2) | P1') = P1 by A1, Def10;
then A4: [#] ((S | P2) | P1') c= [#] S ;
for R being Subset of ((S | P2) | P1') holds
( R in the topology of ((S | P2) | P1') iff ex Q being Subset of S st
( Q in the topology of S & R = Q /\ ([#] ((S | P2) | P1')) ) )

proof

let R be Subset of ((S | P2) | P1'); :: thesis: ( R in the topology of ((S | P2) | P1') iff ex Q being Subset of S st
( Q in the topology of S & R = Q /\ ([#] ((S | P2) | P1')) ) )

A5: now

assume R in the topology of ((S | P2) | P1') ; :: thesis: ex Q being Subset of S st
( Q in the topology of S & R = Q /\ ([#] ((S | P2) | P1')) )
then consider Q0 being Subset of (S | P2) such that
A6: ( Q0 in the topology of (S | P2) & R = Q0 /\ ([#] ((S | P2) | P1')) ) by Def9;
consider Q1 being Subset of S such that
A7: ( Q1 in the topology of S & Q0 = Q1 /\ ([#] (S | P2)) ) by A6, Def9;
R = Q1 /\ (P2 /\ P1) by A2, A3, A6, A7, XBOOLE_1:16
.= Q1 /\ ([#] ((S | P2) | P1')) by A1, A3, XBOOLE_1:28 ;
hence ex Q being Subset of S st
( Q in the topology of S & R = Q /\ ([#] ((S | P2) | P1')) ) by A7; :: thesis: verum

end;

now

given Q being Subset of S such that A8: ( Q in the topology of S & R = Q /\ ([#] ((S | P2) | P1')) ) ; :: thesis: R in the topology of ((S | P2) | P1')
reconsider R' = Q /\ ([#] (S | P2)) as Subset of (S | P2) ;
A9: R' in the topology of (S | P2) by A8, Def9;
R' /\ ([#] ((S | P2) | P1')) = Q /\ (P2 /\ P1) by A2, A3, XBOOLE_1:16
.= R by A1, A3, A8, XBOOLE_1:28 ;
hence R in the topology of ((S | P2) | P1') by A9, Def9; :: thesis: verum

end;

hence ( R in the topology of ((S | P2) | P1') iff ex Q being Subset of S st
( Q in the topology of S & R = Q /\ ([#] ((S | P2) | P1')) ) ) by A5; :: thesis: verum

end;

then (S | P2) | P1' is SubSpace of S by A4, Def9;
hence S | P1 = (S | P2) | P1' by A3, Def10; :: thesis: verum