let L be lower-bounded algebraic LATTICE; :: thesis:

let x, y be Element of L; :: thesis:
assume not y <= x ; :: thesis:
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:
thus p in Irr L by A1, Def4; :: thesis:
thus x <= p by A2; :: thesis:
thus not y <= p by A3; :: thesis:

end;

hence Irr L is order-generating by WAYBEL_6:17; :: thesis:
let X be Subset of L; :: thesis:
assume X is order-generating ; :: thesis:
hence Irr L c= X by Th25; :: thesis: