let L be non empty Poset; :: 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 A1: X is order-generating ; :: thesis: Irr L c= X
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Irr L or x in X )
assume A2: x in Irr L ; :: thesis: x in X
then reconsider x1 = x as Element of L ;
A3: ( x1 = "/\" (((uparrow x1) /\ X),L) & ex_inf_of (uparrow x1) /\ X,L ) by A1, WAYBEL_6:def 5;
x1 is completely-irreducible by A2, Def4;
then x1 in (uparrow x1) /\ X by A3, Th24;
hence x in X by XBOOLE_0:def 4; :: thesis: verum