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 )

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

hence
X is order-generating
by Th17; :: thesis: verum
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;( 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