let R be non empty reflexive transitive RelStr ; :: thesis: for D being non empty directed Subset of (InclPoset (Ids R)) holds sup D = union D
let D be non empty directed Subset of (InclPoset (Ids R)); :: thesis: sup D = union D
A1: ex_sup_of D, InclPoset (Ids R) by WAYBEL_0:75;
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;
( D is_<=_than UD & ( for b being Element of (InclPoset (Ids R)) st b is_>=_than D holds
UD <= b ) ) by Lm1, Lm2;
hence sup D = union D by A1, YELLOW_0:def 9; :: thesis: verum