defpred S₁[ set , set ] means ex x', y' being Element of st
( x' = $1 & y' = $2 & x' << y' );
consider R being Relation of , such that
A1: for x, y being set 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 ;
take R ; :: thesis: for x, y being Element of holds
( [x,y] in R iff x << y )
let x, y be Element of ; :: 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 x', y' being Element of st
( x' = x & y' = y & x' << y' ) 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