reconsider A = {x,y} as non empty Chain of L by A1, ORDERS_2:9;
A2: for z being Element of L st z in A holds
( x <= z & z <= y )

proof

let z be Element of L; :: thesis: ( z in A implies ( x <= z & z <= y ) )
assume A3: z in A ; :: thesis: ( x <= z & z <= y )

per cases ( z = x or z = y ) by A3, TARSKI:def 2;

suppose z = x ; :: thesis: ( x <= z & z <= y )

hence ( x <= z & z <= y ) by A1; :: thesis: verum

end;

suppose z = y ; :: thesis: ( x <= z & z <= y )

hence ( x <= z & z <= y ) by A1; :: thesis: verum

end;

end;

end;

( y in A & x in A ) by TARSKI:def 2;
hence ex b₁ being non empty Chain of L st
( x in b₁ & y in b₁ & ( for z being Element of L st z in b₁ holds
( x <= z & z <= y ) ) ) by A2; :: thesis: verum