let L be lower-bounded algebraic LATTICE; :: thesis: ( Irr L is order-generating & ( for X being Subset of L st X is order-generating holds
Irr L c= X ) )

now :: thesis: for x, y being Element of L st not y <= x holds
ex p being Element of L st
( p in Irr L & x <= p & not y <= p )

let x, y be Element of L; :: thesis: ( not y <= x implies ex p being Element of L st
( p in Irr L & x <= p & not y <= p ) )
assume not y <= x ; :: thesis: ex p being Element of L st
( p in Irr L & x <= p & not y <= p )
then consider p being Element of L such that
A1: p is completely-irreducible and
A2: x <= p and
A3: not y <= p by Th31;
take p = p; :: thesis: ( p in Irr L & x <= p & not y <= p )
thus p in Irr L by A1, Def4; :: thesis: ( x <= p & not y <= p )
thus x <= p by A2; :: thesis: not y <= p
thus not y <= p by A3; :: thesis: verum

end;

hence Irr L is order-generating by WAYBEL_6:17; :: thesis: for X being Subset of L st X is order-generating holds
Irr L c= X
let X be Subset of L; :: thesis: ( X is order-generating implies Irr L c= X )
assume X is order-generating ; :: thesis: Irr L c= X
hence Irr L c= X by Th25; :: thesis: verum