let S be TopSpace; :: thesis: for P1, P2 being Subset of S
for P19 being Subset of (S | P2) st P1 = P19 & P1 c= P2 holds
S | P1 = (S | P2) | P19
let P1, P2 be Subset of S; :: thesis: for P19 being Subset of (S | P2) st P1 = P19 & P1 c= P2 holds
S | P1 = (S | P2) | P19
let P19 be Subset of (S | P2); :: thesis: ( P1 = P19 & P1 c= P2 implies S | P1 = (S | P2) | P19 )
assume that
A1: P1 = P19 and
A2: P1 c= P2 ; :: thesis: S | P1 = (S | P2) | P19
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: ( 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)) ) )

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

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

end;

now :: thesis: ( R in the topology of ((S | P2) | P19) implies ex Q being Subset of S st
( Q in the topology of S & R = Q /\ ([#] ((S | P2) | P19)) ) )

assume R in the topology of ((S | P2) | P19) ; :: thesis: ex Q being Subset of S st
( Q in the topology of S & R = Q /\ ([#] ((S | P2) | P19)) )
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: verum

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: verum

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: verum