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;

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

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 )

thus
Open_setLatt T is lower-bounded
by A1; :: thesis: Bottom (Open_setLatt T) = {} ( 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 r "/\" p = r /\ p by Def3

.= r ; :: thesis: p "/\" r = r

hence p "/\" r = r ; :: thesis: verum

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