set OL = Open_setLatt T;
let p, q be Element of (); :: according to FILTER_0:def 6 :: thesis: ex b1 being Element of the carrier of () st
( p "/\" b1 [= q & ( for b2 being Element of the carrier of () holds
( not p "/\" b2 [= q or b2 [= b1 ) ) )

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 () ;
take r ; :: thesis: ( p "/\" r [= q & ( for b1 being Element of the carrier of () holds
( not p "/\" b1 [= q or b1 [= r ) ) )

A1: p "/\" r = p9 /\ r9 by Def3;
p9 /\ r c= q9 by Th1;
hence p "/\" r [= q by ; :: thesis: for b1 being Element of the carrier of () holds
( not p "/\" b1 [= q or b1 [= r )

let r1 be Element of (); :: 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 ;
then r19 c= r9 by ;
hence r1 [= r by Th7; :: thesis: verum