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 )

thus ( L is distributive implies PRIME L is order-generating ) :: thesis: ( PRIME L is order-generating implies L is distributive )

proof

thus
( PRIME L is order-generating implies L is distributive )
by Th34; :: thesis: verum
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;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