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 )

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

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

proof

hence
( x <= y iff height x <= height y )
by A2; :: thesis: verum
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;then ( x < y or x = y ) by ORDERS_2:def 6;

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