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
end;
hence contradiction by A2; :: thesis: verum
end;
hence ( height x = height y implies x = y ) ; :: thesis: verum