let L be lower-bounded continuous LATTICE; :: thesis: for X being Subset of L st X = (IRR L) \ {(Top L)} holds
X is order-generating
let X be Subset of L; :: thesis: ( X = (IRR L) \ {(Top L)} implies X is order-generating )
assume A1: X = (IRR L) \ {(Top L)} ; :: thesis: X is order-generating
for l1, l2 being Element of L st not l2 <= l1 holds
ex p being Element of L st
( p in X & l1 <= p & not l2 <= p )

proof

let x, y be Element of L; :: thesis: ( not y <= x implies ex p being Element of L st
( p in X & x <= p & not y <= p ) )
assume not y <= x ; :: thesis: ex p being Element of L st
( p in X & x <= p & not y <= p )
then consider p being Element of L such that
A2: p is irreducible and
A3: x <= p and
A4: not y <= p by Th14;
( p <> Top L & p in IRR L ) by A2, A4, Def4, YELLOW_0:45;
then p in X by A1, ZFMISC_1:56;
hence ex p being Element of L st
( p in X & x <= p & not y <= p ) by A3, A4; :: thesis: verum

end;

hence X is order-generating by Th17; :: thesis: verum