let L be D_Lattice; :: thesis: for p, q being Element of (StoneLatt L) holds
( p [= q iff p c= q )
let p, q be Element of (StoneLatt L); :: thesis: ( p [= q iff p c= q )
( ( p [= q implies p "\/" q = q ) & ( p "\/" q = q implies p [= q ) & p "\/" q = p \/ q ) by Def9, LATTICES:def 3;
hence ( p [= q iff p c= q ) by XBOOLE_1:7, XBOOLE_1:12; :: thesis: verum