let T be non empty TopSpace; :: thesis: Open_setLatt T is implicative
set OL = Open_setLatt T;
let p, q be Element of ; :: according to FILTER_0:def 7 :: 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 p' = p, q' = q as Element of Topology_of T ;
Int ((p' ` ) \/ q') is open by TOPS_1:51;
then reconsider r' = Int ((p' ` ) \/ q') as Element of Topology_of T by PRE_TOPC:def 5;
reconsider r = r' as Element of ;
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 = p' /\ r' by Def3;
p' /\ r c= q' by Th1;
hence p "/\" r [= q by A1, Th8; :: 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 ; :: thesis: ( not p "/\" r1 [= q or r1 [= r )
reconsider r2 = r1 as Element of Topology_of T ;
reconsider r1' = r2 as Subset of ;
A2: r1' is open by PRE_TOPC:def 5;
assume A3: p "/\" r1 [= q ; :: thesis: r1 [= r
p "/\" r1 = p' /\ r1' by Def3;
then p' /\ r2 c= q' by A3, Th8;
then r1' c= r' by A2, Th2;
hence r1 [= r by Th8; :: thesis: verum