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 )
A1: ( x in {x,y} & y in {x,y} ) by TARSKI:def 2;
assume A2: x <= y ; :: thesis: {x,y} is Chain of x,y
A3: 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 A4: z in {x,y} ; :: thesis: ( x <= z & z <= y )

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

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

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

end;

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

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

end;

end;

end;

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