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₁ being Element of the carrier of (InclPoset (Ids R)) st
( D is_<=_than b₁ & ( for b₂ being Element of the carrier of (InclPoset (Ids R)) holds
( not D is_<=_than b₂ or b₁ <= 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₁ being Element of the carrier of (InclPoset (Ids R)) holds
( not D is_<=_than b₁ or UD <= b₁ ) ) )
thus ( D is_<=_than UD & ( for b₁ being Element of the carrier of (InclPoset (Ids R)) holds
( not D is_<=_than b₁ or UD <= b₁ ) ) ) by Lm1, Lm2; :: thesis: verum