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

L ~ is completely-distributive by YELLOW_7:51;

hence ( L is distributive & L is continuous & L ~ is continuous ) ; :: thesis: verum