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

proof

let R be Subset of ((S | P2) | P19); :: thesis:

A6: now :: thesis:

given Q being Subset of S such that A7: Q in the topology of S and
A8: R = Q /\ ([#] ((S | P2) | P19)) ; :: thesis:
reconsider R9 = Q /\ ([#] (S | P2)) as Subset of (S | P2) ;
A9: R9 in the topology of (S | P2) by A7, Def4;
R9 /\ ([#] ((S | P2) | P19)) = 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) | P19) by A9, Def4; :: thesis:

end;

now :: thesis:

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

end;

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

end;

[#] ((S | P2) | P19) c= [#] S by A3;
then (S | P2) | P19 is SubSpace of S by A5, Def4;
hence S | P1 = (S | P2) | P19 by A3, Def5; :: thesis: