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 :: thesis: for p being Element of (Open_setLatt T) holds
( r "/\" p = r & p "/\" r = r )

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 by A1; :: thesis: Bottom (Open_setLatt T) = {}
hence Bottom (Open_setLatt T) = {} by A1, LATTICES:def 16; :: thesis: verum