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 that
A2: height x = height y and
A3: x <> y ; :: thesis: contradiction
A4: ( x <= y or y <= x ) by A1, ORDERS_2:11;
height x <> height y

proof

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

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