defpred S₁[ set ] means ex Q being Subset of T st
( Q in the topology of T & $1 = Q /\ P );
consider top1 being Subset-Family of P such that
A1: for Z being Subset of P holds
( Z in top1 iff S₁[Z] ) from SUBSET_1:sch 3();
reconsider top1 = top1 as Subset-Family of P ;
set Y = TopStruct(# P,top1 #);
A2: for Z being Subset of TopStruct(# P,top1 #) holds
( Z in top1 iff ex Q being Subset of T st
( Q in the topology of T & Z = Q /\ ([#] TopStruct(# P,top1 #)) ) )

proof

let Z be Subset of TopStruct(# P,top1 #); :: thesis: ( Z in top1 iff ex Q being Subset of T st
( Q in the topology of T & Z = Q /\ ([#] TopStruct(# P,top1 #)) ) )
thus ( Z in top1 implies ex Q being Subset of T st
( Q in the topology of T & Z = Q /\ ([#] TopStruct(# P,top1 #)) ) ) :: thesis: ( ex Q being Subset of T st
( Q in the topology of T & Z = Q /\ ([#] TopStruct(# P,top1 #)) ) implies Z in top1 )

proof

assume Z in top1 ; :: thesis: ex Q being Subset of T st
( Q in the topology of T & Z = Q /\ ([#] TopStruct(# P,top1 #)) )
then S₁[Z] by A1;
hence ex Q being Subset of T st
( Q in the topology of T & Z = Q /\ ([#] TopStruct(# P,top1 #)) ) ; :: thesis: verum

end;

thus ( ex Q being Subset of T st
( Q in the topology of T & Z = Q /\ ([#] TopStruct(# P,top1 #)) ) implies Z in top1 ) by A1; :: thesis: verum

end;

[#] TopStruct(# P,top1 #) c= [#] T ;
then reconsider Y = TopStruct(# P,top1 #) as strict SubSpace of T by A2, Def4;
take Y ; :: thesis: [#] Y = P
thus [#] Y = P ; :: thesis: verum