defpred S₁[ 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 & S₁[x,y] ) ) from RELSET_1:sch 1();
reconsider R = R as Relation of L ;
take R ; :: thesis: for x, y being Element of L holds
( [x,y] in R iff x << y )
let x, y be Element of L; :: thesis: ( [x,y] in R iff x << y )

hereby :: thesis: ( x << y implies [x,y] in R )

assume [x,y] in R ; :: thesis: x << y
then ex x9, y9 being Element of L st
( x9 = x & y9 = y & x9 << y9 ) by A1;
hence x << y ; :: thesis: verum

end;

assume x << y ; :: thesis: [x,y] in R
hence [x,y] in R by A1; :: thesis: verum