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
A1: {(Bottom L),x} is Chain of Bottom L,x by Th1, YELLOW_0:44;
then A2: card {(Bottom L),x} <= height x by Def3;
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:57;
hence height x >= 1 by A2, XXREAL_0:2; :: thesis: verum
end;
suppose A3: x = Bottom L ; :: thesis: height x >= 1
A4: {(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;
{(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;
then A5: {(Bottom L),(Bottom L)} = {(Bottom L)} by A4, XBOOLE_0:def 10;
card {(Bottom L),(Bottom L)} <= height (Bottom L) by A1, A3, Def3;
hence height x >= 1 by A3, A5, CARD_1:30; :: thesis: verum
end;
end;