defpred S1[ object , object ] means ex x9, y9 being Element of L st
( x9 = $1 & y9 = $2 & x9 << y9 );
consider R being Relation of the carrier of L, the carrier of L such that
A1:
for x, y being object holds
( [x,y] in R iff ( x in the carrier of L & y in the carrier of L & S1[x,y] ) )
from RELSET_1:sch 1();
reconsider R = R as Relation of L ;
take
R
; for x, y being Element of L holds
( [x,y] in R iff x << y )
let x, y be Element of L; ( [x,y] in R iff x << y )
hereby ( x << y implies [x,y] in R )
assume
[x,y] in R
;
x << ythen
ex
x9,
y9 being
Element of
L st
(
x9 = x &
y9 = y &
x9 << y9 )
by A1;
hence
x << y
;
verum
end;
assume
x << y
; [x,y] in R
hence
[x,y] in R
by A1; verum