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 implies height x = height y ) ; :: thesis: ( height x = height y implies x = y )
( height x = height y implies x = y )

proof

assume A2: ( height x = height y & x <> y ) ; :: thesis: contradiction
then A3: ( ( x <= y or y <= x ) & x <> y ) by A1, ORDERS_2:38;
height x <> height y

proof

per cases ( x < y or y < x ) by A3, ORDERS_2:def 10;

suppose x < y ; :: thesis: height x <> height y

hence height x <> height y by A1, Th3; :: thesis: verum

end;

suppose y < x ; :: thesis: height x <> height y

hence height x <> height y by A1, Th3; :: thesis: verum

end;

end;

end;

hence contradiction by A2; :: thesis: verum

end;

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