let R be RelStr ; :: thesis: ( R is empty implies R is real )
assume A1: the carrier of R is empty ; :: according to STRUCT_0:def 1 :: thesis: R is real
hence the carrier of R c= REAL ; :: according to LFUZZY_0:def 1 :: thesis: for x, y being Real st x in the carrier of R & y in the carrier of R holds
( [x,y] in the InternalRel of R iff x <= y )
thus for x, y being Real st x in the carrier of R & y in the carrier of R holds
( [x,y] in the InternalRel of R iff x <= y ) by A1; :: thesis: verum