let L be finite LATTICE; :: thesis: for x being Element of L holds
( height x = 1 iff x = Bottom L )
let x be Element of L; :: thesis: ( height x = 1 iff x = Bottom L )
A1: ( x = Bottom L implies height x = 1 )

proof

A2: for B being Chain of Bottom L, Bottom L holds B = {(Bottom L)}

proof

let B be Chain of Bottom L, Bottom L; :: thesis: B = {(Bottom L)}
A3: B c= {(Bottom L)}

proof

let r be set ; :: according to LATTICE7:def 1 :: thesis: ( r is Element of L & r in B implies r in {(Bottom L)} )
( r in B implies r in {(Bottom L)} )

proof

assume r in B ; :: thesis: r in {(Bottom L)}
then reconsider r = r as Element of B ;
( Bottom L <= r & r <= Bottom L ) by Def2;
then Bottom L = r by ORDERS_2:2;
hence r in {(Bottom L)} by TARSKI:def 1; :: thesis: verum

end;

hence ( r is Element of L & r in B implies r in {(Bottom L)} ) ; :: thesis: verum

end;

{(Bottom L)} c= B

proof

let r be set ; :: according to LATTICE7:def 1 :: thesis: ( r is Element of L & r in {(Bottom L)} implies r in B )
( r in {(Bottom L)} implies r in B )

proof

assume r in {(Bottom L)} ; :: thesis: r in B
then r = Bottom L by TARSKI:def 1;
hence r in B by Def2; :: thesis: verum

end;

hence ( r is Element of L & r in {(Bottom L)} implies r in B ) ; :: thesis: verum

end;

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

end;

assume A4: x = Bottom L ; :: thesis: height x = 1
( ex A being Chain of Bottom L, Bottom L st height (Bottom L) = card A & card {(Bottom L)} = 1 ) by Def3, CARD_1:30;
hence height x = 1 by A4, A2; :: thesis: verum

end;

( height x = 1 implies x = Bottom L )

proof

A5: for z being Element of L st z in {(Bottom L),x} holds
( Bottom L <= z & z <= x )

proof

let z be Element of L; :: thesis: ( z in {(Bottom L),x} implies ( Bottom L <= z & z <= x ) )
assume A6: z in {(Bottom L),x} ; :: thesis: ( Bottom L <= z & z <= x )

per cases ( z = Bottom L or z = x ) by A6, TARSKI:def 2;

suppose z = Bottom L ; :: thesis: ( Bottom L <= z & z <= x )

hence ( Bottom L <= z & z <= x ) by YELLOW_0:44; :: thesis: verum

end;

suppose z = x ; :: thesis: ( Bottom L <= z & z <= x )

hence ( Bottom L <= z & z <= x ) by YELLOW_0:44; :: thesis: verum

end;

end;

end;

A7: ( x in {(Bottom L),x} & Bottom L in {(Bottom L),x} ) by TARSKI:def 2;
A8: Bottom L <= x by YELLOW_0:44;
then {(Bottom L),x} is Chain of L by ORDERS_2:9;
then A9: {(Bottom L),x} is Chain of Bottom L,x by A8, A7, A5, Def2;
assume that
A10: height x = 1 and
A11: x <> Bottom L ; :: thesis: contradiction
card {(Bottom L),x} = 2 by A11, CARD_2:57;
hence contradiction by A10, A9, Def3; :: thesis: verum

end;

hence ( height x = 1 iff x = Bottom L ) by A1; :: thesis: verum