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 = {()}
proof
let B be Chain of Bottom L, Bottom L; :: thesis: B = {()}
A3: B c= {()}
proof
let r be set ; :: according to LATTICE7:def 1 :: thesis: ( r is Element of L & r in B implies r in {()} )
( r in B implies r in {()} )
proof
assume r in B ; :: thesis: r in {()}
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 {()} by TARSKI:def 1; :: thesis: verum
end;
hence ( r is Element of L & r in B implies r in {()} ) ; :: thesis: verum
end;
{()} c= B
proof
let r be set ; :: according to LATTICE7:def 1 :: thesis: ( r is Element of L & r in {()} implies r in B )
( r in {()} implies r in B )
proof
assume r in {()} ; :: 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 {()} implies r in B ) ; :: thesis: verum
end;
hence B = {()} by ; :: thesis: verum
end;
assume A4: x = Bottom L ; :: thesis: height x = 1
( ex A being Chain of Bottom L, Bottom L st height () = card A & card {()} = 1 ) by ;
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 {(),x} holds
( Bottom L <= z & z <= x )
proof
let z be Element of L; :: thesis: ( z in {(),x} implies ( Bottom L <= z & z <= x ) )
assume A6: z in {(),x} ; :: thesis: ( Bottom L <= z & z <= x )
per cases ( z = Bottom L or z = x ) by ;
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 {(),x} & Bottom L in {(),x} ) by TARSKI:def 2;
A8: Bottom L <= x by YELLOW_0:44;
then {(),x} is Chain of L by ORDERS_2:9;
then A9: {(),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 {(),x} = 2 by ;
hence contradiction by A10, A9, Def3; :: thesis: verum
end;
hence ( height x = 1 iff x = Bottom L ) by A1; :: thesis: verum