let X be real-membered set ; :: thesis: ex R being strict RelStr st

( the carrier of R = X & R is real )

( the carrier of R = X & R is real )

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

end;

suppose A1:
X is empty
; :: thesis: ex R being strict RelStr st

( the carrier of R = X & R is real )

( 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;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

suppose
not X is empty
; :: thesis: ex R being strict RelStr st

( the carrier of R = X & R is real )

( the carrier of R = X & R is real )

then reconsider Y = X as non empty set ;

defpred S_{1}[ 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_{1}[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;defpred S

( $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

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