let L be non empty finite lower-bounded LATTICE; :: thesis: ( L is flat iff for x being Element of L holds height x <= 2 )

hereby :: thesis: ( ( for x being Element of L holds height x <= 2 ) implies L is flat )

assume A0: L is flat ; :: thesis: for x being Element of L holds height b₂ <= 2
let x be Element of L; :: thesis: height b₁ <= 2
S0: Bottom L <= x by YELLOW_0:44;
reconsider D = {(Bottom L),x} as Chain of Bottom L,x by LATTICE7:1, YELLOW_0:44;

per cases ( Bottom L <> x or Bottom L = x ) ;

suppose KK: Bottom L <> x ; :: thesis: height b₁ <= 2

then t1: card D = 2 by CARD_2:57;
for A being Chain of Bottom L,x holds card A <= 2

proof

let A be Chain of Bottom L,x; :: thesis: card A <= 2
consider b being Element of L such that
H1: ( A = {b} or A = {(Bottom L),b} ) by Thflat01, A0;
H2: ( x in A & Bottom L in A ) by LATTICE7:def 2, S0;
A <> {b}

proof

assume A = {b} ; :: thesis: contradiction
then ( x = b & b = Bottom L ) by TARSKI:def 1, H2;
hence contradiction by KK; :: thesis: verum

end;

hence card A <= 2 by CARD_2:50, H1; :: thesis: verum

end;

hence height x <= 2 by LATTICE7:def 3, t1; :: thesis: verum

end;

suppose Bottom L = x ; :: thesis: height b₁ <= 2

then height x = 1 by LATTICE7:6;
hence height x <= 2 ; :: thesis: verum

end;

end;

end;

assume AA: for x being Element of L holds height x <= 2 ; :: thesis: L is flat
ex a being Element of L st
for x, y being Element of L holds
( x <= y iff ( x = a or x = y ) )

proof

take a = Bottom L; :: thesis: for x, y being Element of L holds
( x <= y iff ( x = a or x = y ) )
let x, y be Element of L; :: thesis: ( x <= y iff ( x = a or x = y ) )

hereby :: thesis: ( ( x = a or x = y ) implies x <= y )

assume AS: x <= y ; :: thesis: ( x = a or x = y )

per cases ( ( x = a & y = x ) or ( x <> a & y = x ) or ( x <> a & y <> x ) or ( x = a & y <> x ) ) ;

suppose ( x = a & y = x ) ; :: thesis: ( x = a or x = y )

hence ( x = a or x = y ) ; :: thesis: verum

end;

suppose ( x <> a & y = x ) ; :: thesis: ( x = a or x = y )

hence ( x = a or x = y ) ; :: thesis: verum

end;

suppose a1: ( x <> a & y <> x ) ; :: thesis: ( x = a or x = y )

then a < x by YELLOW_0:44;
then height a < height x by LATTICE7:2;
then 1 < height x by LATTICE7:6;
then y1: 1 + 1 <= height x by NAT_1:13;
x < y by a1, AS;
then Y2: height x < height y by LATTICE7:2;
height x <= 2 by AA;
then height x = 2 by y1, XXREAL_0:1;
hence ( x = a or x = y ) by AA, Y2; :: thesis: verum

end;

suppose ( x = a & y <> x ) ; :: thesis: ( x = a or x = y )

hence ( x = a or x = y ) ; :: thesis: verum

end;

end;

end;

thus ( ( x = a or x = y ) implies x <= y ) by YELLOW_0:44; :: thesis: verum

end;

hence L is flat ; :: thesis: verum