for S being TopStruct ex T being TopExtension of S st
( T is strict & the topology of S is prebasis of T )