let L be lower-bounded continuous LATTICE; :: thesis:
let X be Subset of L; :: thesis:
assume A1: X = (IRR L) \ {(Top L)} ; :: thesis:
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 )

let x, y be Element of L; :: thesis:
assume not y <= x ; :: thesis:
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:

end;