set X = {0};
reconsider O = 0 as Element of {0} by TARSKI:def 1;
set F = the BinOp of {0};
set G = the Function of [:REAL,{0}:],{0};
set N = the Function of {0},REAL;
take RT = RLNormTopStruct(# {0},O, the BinOp of {0}, the Function of [:REAL,{0}:],{0},({} (bool {0})), the Function of {0},REAL #); :: thesis: ( RT is strict & not RT is empty )
thus RT is strict ; :: thesis: not RT is empty
thus not the carrier of RT is empty ; :: according to STRUCT_0:def 1 :: thesis: verum