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