let T be non empty TopSpace; :: thesis: ( Open_setLatt T is lower-bounded & Bottom (Open_setLatt T) = {} )
set OL = Open_setLatt T;
reconsider r = {} as Element of (Open_setLatt T) by PRE_TOPC:1;

A1: now

let p be Element of (Open_setLatt T); :: thesis: ( r "/\" p = r & p "/\" r = r )
thus r "/\" p = r /\ p by Def3
.= r ; :: thesis: p "/\" r = r
hence p "/\" r = r ; :: thesis: verum

end;

thus Open_setLatt T is lower-bounded :: thesis: Bottom (Open_setLatt T) = {}

proof

take r ; :: according to LATTICES:def 13 :: thesis: for b₁ being Element of the carrier of (Open_setLatt T) holds
( r "/\" b₁ = r & b₁ "/\" r = r )
thus for b₁ being Element of the carrier of (Open_setLatt T) holds
( r "/\" b₁ = r & b₁ "/\" r = r ) by A1; :: thesis: verum

end;

hence Bottom (Open_setLatt T) = {} by A1, LATTICES:def 16; :: thesis: verum