let T be non empty TopSpace; :: thesis: for p, q being Element of holds
( p [= q iff p c= q )
let p, q be Element of ; :: thesis: ( p [= q iff p c= q )
A1: ( p [= q iff p "\/" q = q ) by LATTICES:def 3;
p "\/" q = p \/ q by Def2;
hence ( p [= q iff p c= q ) by A1, XBOOLE_1:7, XBOOLE_1:12; :: thesis: verum