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 )

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

{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

{x,y} is Chain of L
by A2, ORDERS_2:9;
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 )

end;assume A4: z in {x,y} ; :: thesis: ( x <= z & z <= y )

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