set X = {0 };
reconsider O = 0 as Element of {0 } by TARSKI:def 1;
consider F being BinOp of {0 };
consider G being Function of [:REAL ,{0 }:],{0 };
take RT = RLTopStruct(# {0 },O,F,G,({} (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