set EX = the non empty TopStruct ;
set C = the carrier of the non empty TopStruct ;
set T = the topology of the non empty TopStruct ;
set F = the Function of (bool the carrier of the non empty TopStruct ),(bool the carrier of the non empty TopStruct );
take TT = 2TopStruct(# the carrier of the non empty TopStruct , the Function of (bool the carrier of the non empty TopStruct ),(bool the carrier of the non empty TopStruct ), the topology of the non empty TopStruct #); :: thesis: ( not TT is empty & TT is strict )
thus ( not TT is empty & TT is strict ) ; :: thesis: verum