theorem :: OPENLATT:25

for L being D_Lattice
for p, q being Element of (StoneLatt L) holds
( p "\/" q = p \/ q & p "/\" q = p /\ q ) by Def9, Def10;