let L be finite LATTICE; :: thesis: for C being Chain of L
for x, y being Element of L st x in C & y in C holds
( x <= y iff height x <= height y )
let C be Chain of L; :: thesis: for x, y being Element of L st x in C & y in C holds
( x <= y iff height x <= height y )
let x, y be Element of L; :: thesis: ( x in C & y in C implies ( x <= y iff height x <= height y ) )
assume A1: ( x in C & y in C ) ; :: thesis: ( x <= y iff height x <= height y )
A2: ( height x <= height y implies x <= y )

proof

assume height x <= height y ; :: thesis: x <= y
then ( height x < height y or height x = height y ) by XXREAL_0:1;
then ( x < y or height x = height y ) by A1, Th3;
hence x <= y by A1, Th4, ORDERS_2:def 6; :: thesis: verum

end;

( x <= y implies height x <= height y )

proof

assume x <= y ; :: thesis: height x <= height y
then ( x < y or x = y ) by ORDERS_2:def 6;
hence height x <= height y by A1, Th3; :: thesis: verum

end;

hence ( x <= y iff height x <= height y ) by A2; :: thesis: verum