let L be LATTICE; :: thesis: for x, y being Element of L st x <= y holds
{x,y} is Chain of x,y
let x, y be Element of L; :: thesis: ( x <= y implies {x,y} is Chain of x,y )
assume A1: x <= y ; :: thesis: {x,y} is Chain of x,y
then A2: {x,y} is Chain of L by ORDERS_2:36;
A3: x in {x,y} by TARSKI:def 2;
A4: y in {x,y} by TARSKI:def 2;
for z being Element of L st z in {x,y} holds
( x <= z & z <= y )

proof

let z be Element of L; :: thesis: ( z in {x,y} implies ( x <= z & z <= y ) )
assume A5: z in {x,y} ; :: thesis: ( x <= z & z <= y )

per cases ( z = x or z = y ) by A5, 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;

hence {x,y} is Chain of x,y by A1, A2, A3, A4, Def2; :: thesis: verum