set I = InclPoset (Ids R);

let D be non empty directed Subset of (InclPoset (Ids R)); :: according to WAYBEL_0:def 39 :: thesis: ex b_{1} being Element of the carrier of (InclPoset (Ids R)) st

( D is_<=_than b_{1} & ( for b_{2} being Element of the carrier of (InclPoset (Ids R)) holds

( not D is_<=_than b_{2} or b_{1} <= b_{2} ) ) )

reconsider UD = union D as Ideal of R by Th2;

UD in Ids R ;

then reconsider UD = UD as Element of (InclPoset (Ids R)) by YELLOW_1:1;

take UD ; :: thesis: ( D is_<=_than UD & ( for b_{1} being Element of the carrier of (InclPoset (Ids R)) holds

( not D is_<=_than b_{1} or UD <= b_{1} ) ) )

thus ( D is_<=_than UD & ( for b_{1} being Element of the carrier of (InclPoset (Ids R)) holds

( not D is_<=_than b_{1} or UD <= b_{1} ) ) )
by Lm1, Lm2; :: thesis: verum

let D be non empty directed Subset of (InclPoset (Ids R)); :: according to WAYBEL_0:def 39 :: thesis: ex b

( D is_<=_than b

( not D is_<=_than b

reconsider UD = union D as Ideal of R by Th2;

UD in Ids R ;

then reconsider UD = UD as Element of (InclPoset (Ids R)) by YELLOW_1:1;

take UD ; :: thesis: ( D is_<=_than UD & ( for b

( not D is_<=_than b

thus ( D is_<=_than UD & ( for b

( not D is_<=_than b