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

proof

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

A6: now

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

end;

now

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

end;

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

end;

[#] ((S | P2) | P1') c= [#] S by A3;
then (S | P2) | P1' is SubSpace of S by A5, Def9;
hence S | P1 = (S | P2) | P1' by A3, Def10; :: thesis: verum