:: deftheorem Def1 defines real LFUZZY_0:def 1 :
for R being RelStr holds
( R is real iff ( the carrier of R c= REAL & ( 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 ) ) ) );