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 )
thus ( x < y iff height x < height y ) :: thesis: verum

proof

thus ( x < y implies height x < height y ) by Th2; :: thesis: ( height x < height y implies x < y )
( height x < height y implies x < y )

proof

assume A2: height x < height y ; :: thesis: x < y

per cases ( x <= y or y <= x ) by A1, ORDERS_2:38;

suppose x <= y ; :: thesis: x < y

hence x < y by A2, ORDERS_2:def 10; :: thesis: verum

end;

suppose y <= x ; :: thesis: x < y

then ( x = y or y < x ) by ORDERS_2:def 10;
hence x < y by A2, Th2; :: thesis: verum

end;

end;

end;

hence ( height x < height y implies x < y ) ; :: thesis: verum

end;