consider ZS being non empty set , O being Element of ZS, F being BinOp of ZS, G being Function of [:REAL ,ZS:],ZS;
take RLSStruct(# ZS,O,F,G #) ; :: thesis: not RLSStruct(# ZS,O,F,G #) is empty
thus not the carrier of RLSStruct(# ZS,O,F,G #) is empty ; :: according to STRUCT_0:def 1 :: thesis: verum