let S be TopStruct ; :: thesis: ex T being TopExtension of S st
( T is strict & the topology of S is prebasis of T )
consider T being strict TopSpace such that
A1: the carrier of T = the carrier of S and
A2: the topology of S is prebasis of T by Lm1;
the topology of S c= the topology of T by A2, TOPS_2:64;
then reconsider T = T as TopExtension of S by A1, Def5;
take T ; :: thesis: ( T is strict & the topology of S is prebasis of T )
thus ( T is strict & the topology of S is prebasis of T ) by A2; :: thesis: verum