let X be real-membered set ; :: thesis: ex R being strict RelStr st
( the carrier of R = X & R is real )

per cases ( X is empty or not X is empty ) ;

suppose A1: X is empty ; :: thesis: ex R being strict RelStr st
( the carrier of R = X & R is real )

set E = the empty strict RelStr ;
take the empty strict RelStr ; :: thesis: ( the carrier of the empty strict RelStr = X & the empty strict RelStr is real )
thus ( the carrier of the empty strict RelStr = X & the empty strict RelStr is real ) by A1; :: thesis: verum

end;

suppose not X is empty ; :: thesis: ex R being strict RelStr st
( the carrier of R = X & R is real )

then reconsider Y = X as non empty set ;
defpred S₁[ set , set ] means ex x, y being Real st
( $1 = x & $2 = y & x <= y );
consider L being non empty strict RelStr such that
A2: the carrier of L = Y and
A3: for a, b being Element of L holds
( a <= b iff S₁[a,b] ) from YELLOW_0:sch 1();
take L ; :: thesis: ( the carrier of L = X & L is real )
thus the carrier of L = X by A2; :: thesis: L is real
thus the carrier of L c= REAL by A2, MEMBERED:3; :: according to LFUZZY_0:def 1 :: thesis: for x, y being Real st x in the carrier of L & y in the carrier of L holds
( [x,y] in the InternalRel of L iff x <= y )
let x, y be Real; :: thesis: ( x in the carrier of L & y in the carrier of L implies ( [x,y] in the InternalRel of L iff x <= y ) )
assume ( x in the carrier of L & y in the carrier of L ) ; :: thesis: ( [x,y] in the InternalRel of L iff x <= y )
then reconsider a = x, b = y as Element of L ;
( a <= b iff [x,y] in the InternalRel of L ) by ORDERS_2:def 5;
then ( [x,y] in the InternalRel of L iff ex x, y being Real st
( a = x & b = y & x <= y ) ) by A3;
hence ( [x,y] in the InternalRel of L iff x <= y ) ; :: thesis: verum

end;

end;