let L be lower-bounded continuous LATTICE; :: thesis: ( L is distributive iff PRIME L is order-generating )
thus ( L is distributive implies PRIME L is order-generating ) :: thesis: ( PRIME L is order-generating implies L is distributive )

proof

assume L is distributive ; :: thesis: PRIME L is order-generating
then A1: PRIME L = IRR L by Th28;
(IRR L) \ {(Top L)} c= IRR L by XBOOLE_1:36;
hence PRIME L is order-generating by A1, Th18, Th19; :: thesis: verum

end;

thus ( PRIME L is order-generating implies L is distributive ) by Th34; :: thesis: verum