set OL = Open_setLatt T;
let p, q be Element of (Open_setLatt T); :: according to FILTER_0:def 6 :: thesis: ex b₁ being Element of the carrier of (Open_setLatt T) st
( p "/\" b₁ [= q & ( for b₂ being Element of the carrier of (Open_setLatt T) holds
( not p "/\" b₂ [= q or b₂ [= 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₁ being Element of the carrier of (Open_setLatt T) holds
( not p "/\" b₁ [= q or b₁ [= r ) ) )
A1: p "/\" r = p9 /\ r9 by Def3;
p9 /\ r c= q9 by Th1;
hence p "/\" r [= q by A1, Th7; :: thesis: for b₁ being Element of the carrier of (Open_setLatt T) holds
( not p "/\" b₁ [= q or b₁ [= 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