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 & the topology of S is prebasis of T ) by Lm2;
the topology of S c= the topology of T by A1, CANTOR_1:def 5;
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 A1; :: thesis: verum