let L be non empty finite LATTICE; :: thesis: for x being Element of L holds height x >= 1
let x be Element of L; :: thesis: height x >= 1
( ex A being Chain of Bottom L,x st height x = card A & ( for A being Chain of Bottom L,x holds card A <= height x ) ) by Def3;
then consider A being Chain of Bottom L,x such that
height x = card A and
A1: for B being Chain of Bottom L,x holds card B <= height x ;
A2: {(Bottom L),x} is Chain of Bottom L,x by Th1, YELLOW_0:44;
then A3: card {(Bottom L),x} <= height x by A1;

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

suppose x <> Bottom L ; :: thesis: height x >= 1

then card {(Bottom L),x} = 2 by CARD_2:76;
hence height x >= 1 by A3, XXREAL_0:2; :: thesis: verum

end;

suppose A4: x = Bottom L ; :: thesis: height x >= 1

then A5: card {(Bottom L),(Bottom L)} <= height (Bottom L) by A1, A2;
{(Bottom L),(Bottom L)} = {(Bottom L)}

proof

A6: {(Bottom L),(Bottom L)} c= {(Bottom L)}

proof

let d be Element of L; :: according to LATTICE7:def 1 :: thesis: ( d in {(Bottom L),(Bottom L)} implies d in {(Bottom L)} )
assume d in {(Bottom L),(Bottom L)} ; :: thesis: d in {(Bottom L)}
then ( d = Bottom L or d = Bottom L ) by TARSKI:def 2;
hence d in {(Bottom L)} by TARSKI:def 1; :: thesis: verum

end;

{(Bottom L)} c= {(Bottom L),(Bottom L)}

proof

let d be Element of L; :: according to LATTICE7:def 1 :: thesis: ( d in {(Bottom L)} implies d in {(Bottom L),(Bottom L)} )
assume d in {(Bottom L)} ; :: thesis: d in {(Bottom L),(Bottom L)}
then d = Bottom L by TARSKI:def 1;
hence d in {(Bottom L),(Bottom L)} by TARSKI:def 2; :: thesis: verum

end;

hence {(Bottom L),(Bottom L)} = {(Bottom L)} by A6, XBOOLE_0:def 10; :: thesis: verum

end;

hence height x >= 1 by A4, A5, CARD_1:50; :: thesis: verum

end;

end;