set OL = Open_setLatt T;

let p, q be Element of (Open_setLatt T); :: according to FILTER_0:def 6 :: thesis: ex b_{1} being Element of the carrier of (Open_setLatt T) st

( p "/\" b_{1} [= q & ( for b_{2} being Element of the carrier of (Open_setLatt T) holds

( not p "/\" b_{2} [= q or b_{2} [= b_{1} ) ) )

reconsider p9 = p, q9 = q as Element of Topology_of T ;

reconsider r9 = Int ((p9 `) \/ q9) as Element of Topology_of T by PRE_TOPC:def 2;

reconsider r = r9 as Element of (Open_setLatt T) ;

take r ; :: thesis: ( p "/\" r [= q & ( for b_{1} being Element of the carrier of (Open_setLatt T) holds

( not p "/\" b_{1} [= q or b_{1} [= r ) ) )

A1: p "/\" r = p9 /\ r9 by Def3;

p9 /\ r c= q9 by Th1;

hence p "/\" r [= q by A1, Th7; :: thesis: for b_{1} being Element of the carrier of (Open_setLatt T) holds

( not p "/\" b_{1} [= q or b_{1} [= r )

let r1 be Element of (Open_setLatt T); :: thesis: ( not p "/\" r1 [= q or r1 [= r )

reconsider r2 = r1 as Element of Topology_of T ;

reconsider r19 = r2 as Subset of T ;

A2: r19 is open ;

assume A3: p "/\" r1 [= q ; :: thesis: r1 [= r

p "/\" r1 = p9 /\ r19 by Def3;

then p9 /\ r2 c= q9 by A3, Th7;

then r19 c= r9 by A2, Th2;

hence r1 [= r by Th7; :: thesis: verum

let p, q be Element of (Open_setLatt T); :: according to FILTER_0:def 6 :: thesis: ex b

( p "/\" b

( not p "/\" b

reconsider p9 = p, q9 = q as Element of Topology_of T ;

reconsider r9 = Int ((p9 `) \/ q9) as Element of Topology_of T by PRE_TOPC:def 2;

reconsider r = r9 as Element of (Open_setLatt T) ;

take r ; :: thesis: ( p "/\" r [= q & ( for b

( not p "/\" b

A1: p "/\" r = p9 /\ r9 by Def3;

p9 /\ r c= q9 by Th1;

hence p "/\" r [= q by A1, Th7; :: thesis: for b

( not p "/\" b

let r1 be Element of (Open_setLatt T); :: thesis: ( not p "/\" r1 [= q or r1 [= r )

reconsider r2 = r1 as Element of Topology_of T ;

reconsider r19 = r2 as Subset of T ;

A2: r19 is open ;

assume A3: p "/\" r1 [= q ; :: thesis: r1 [= r

p "/\" r1 = p9 /\ r19 by Def3;

then p9 /\ r2 c= q9 by A3, Th7;

then r19 c= r9 by A2, Th2;

hence r1 [= r by Th7; :: thesis: verum