let X be real-membered set ; 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
not
X is
empty
;
ex R being strict RelStr st
( the carrier of R = X & R is real )then reconsider Y =
X as non
empty set ;
defpred S1[
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
S1[
a,
b] )
from YELLOW_0:sch 1();
take
L
;
( the carrier of L = X & L is real )thus
the
carrier of
L = X
by A2;
L is real thus
the
carrier of
L c= REAL
by A2, MEMBERED:3;
LFUZZY_0:def 1 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;
( 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 )
;
( [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 )
;
verum end;