let T be non empty TopSpace; :: thesis: for p, q being Element of (Open_setLatt T) holds

( p [= q iff p c= q )

let p, q be Element of (Open_setLatt T); :: thesis: ( p [= q iff p c= q )

p "\/" q = p \/ q by Def2;

hence ( p [= q iff p c= q ) by XBOOLE_1:7, XBOOLE_1:12; :: thesis: verum

( p [= q iff p c= q )

let p, q be Element of (Open_setLatt T); :: thesis: ( p [= q iff p c= q )

p "\/" q = p \/ q by Def2;

hence ( p [= q iff p c= q ) by XBOOLE_1:7, XBOOLE_1:12; :: thesis: verum