let T be non empty TopSpace; :: thesis: for p, q being Element of (Open_setLatt T)
for p9, q9 being Element of Topology_of T st p = p9 & q = q9 holds
( p [= q iff p9 c= q9 )
let p, q be Element of (Open_setLatt T); :: thesis: for p9, q9 being Element of Topology_of T st p = p9 & q = q9 holds
( p [= q iff p9 c= q9 )
let p9, q9 be Element of Topology_of T; :: thesis: ( p = p9 & q = q9 implies ( p [= q iff p9 c= q9 ) )
assume that
A1: p = p9 and
A2: q = q9 ; :: thesis: ( p [= q iff p9 c= q9 )

hereby :: thesis: ( p9 c= q9 implies p [= q )

assume A3: p [= q ; :: thesis: p9 c= q9
p9 \/ q9 = p "\/" q by A1, A2, Def2
.= q9 by A2, A3, LATTICES:def 3 ;
hence p9 c= q9 by XBOOLE_1:7; :: thesis: verum

end;

assume A4: p9 c= q9 ; :: thesis: p [= q
p "\/" q = p9 \/ q9 by A1, A2, Def2
.= q by A2, A4, XBOOLE_1:12 ;
hence p [= q by LATTICES:def 3; :: thesis: verum