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 )

( 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

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

( 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;proof

assume A4:
x = Bottom L
; :: thesis: height x = 1
let B be Chain of Bottom L, Bottom L; :: thesis: B = {(Bottom L)}

A3: B c= {(Bottom L)}

end;A3: B c= {(Bottom L)}

proof

{(Bottom L)} c= B
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)} )

end;( r in B implies r in {(Bottom L)} )

proof

hence
( r is Element of L & r in B implies r in {(Bottom L)} )
; :: thesis: verum
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;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

proof

hence
B = {(Bottom L)}
by A3, XBOOLE_0:def 10; :: thesis: verum
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 )

end;( r in {(Bottom L)} implies r in B )

proof

hence
( r is Element of L & r in {(Bottom L)} implies r in B )
; :: thesis: verum
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;then r = Bottom L by TARSKI:def 1;

hence r in B by Def2; :: thesis: verum

( 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

proof

hence
( height x = 1 iff x = Bottom L )
by A1; :: thesis: verum
A5:
for z being Element of L st z in {(Bottom L),x} holds

( Bottom L <= z & z <= x )

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;( Bottom L <= z & z <= x )

proof

A7:
( x in {(Bottom L),x} & Bottom L in {(Bottom L),x} )
by TARSKI:def 2;
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 )

end;assume A6: z in {(Bottom L),x} ; :: thesis: ( Bottom L <= z & z <= x )

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