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

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