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: ( height x = 1 implies x = Bottom L )

proof

assume A2: ( height x = 1 & x <> Bottom L ) ; :: thesis: contradiction
( 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
A3: ( height x = card A & ( for A being Chain of Bottom L,x holds card A <= height x ) ) ;
A4: {(Bottom L),x} is Chain of Bottom L,x

proof

A5: Bottom L <= x by YELLOW_0:44;
then A6: {(Bottom L),x} is Chain of L by ORDERS_2:36;
A7: x in {(Bottom L),x} by TARSKI:def 2;
A8: Bottom L in {(Bottom L),x} by TARSKI:def 2;
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 A9: z in {(Bottom L),x} ; :: thesis: ( Bottom L <= z & z <= x )

per cases ( z = Bottom L or z = x ) by A9, 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;

hence {(Bottom L),x} is Chain of Bottom L,x by A5, A6, A7, A8, Def2; :: thesis: verum

end;

card {(Bottom L),x} = 2 by A2, CARD_2:76;
hence contradiction by A2, A3, A4; :: thesis: verum

end;

( x = Bottom L implies height x = 1 )

proof

assume A10: x = Bottom L ; :: thesis: height x = 1
( ex A being Chain of Bottom L, Bottom L st height (Bottom L) = card A & ( for A being Chain of Bottom L, Bottom L holds card A <= height (Bottom L) ) ) by Def3;
then consider A being Chain of Bottom L, Bottom L such that
A11: ( height (Bottom L) = card A & ( for A being Chain of Bottom L, Bottom L holds card A <= height (Bottom L) ) ) ;
A12: 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)}
A13: 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:25;
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 A13, XBOOLE_0:def 10; :: thesis: verum

end;

card {(Bottom L)} = 1 by CARD_1:50;
hence height x = 1 by A10, A11, A12; :: thesis: verum

end;

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