let L be complete completely-distributive LATTICE; :: thesis: ( L is distributive & L is continuous & L ~ is continuous )
L ~ is completely-distributive by YELLOW_7:51;
hence ( L is distributive & L is continuous & L ~ is continuous ) ; :: thesis: verum