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};
take RT = RLTopStruct(# {0},O, the BinOp of {0}, the Function of [:REAL,{0}:],{0},({} (bool {0})) #); :: 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