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
reconsider UD = union D as Ideal of R by Th2;
A1: ex_sup_of D, InclPoset (Ids R) by WAYBEL_0:75;
UD in Ids R ;
then reconsider UD = UD as Element of (InclPoset (Ids R)) by YELLOW_1:1;
A2: for b being Element of (InclPoset (Ids R)) st b is_>=_than D holds
UD <= b by Lm2;
D is_<=_than UD by Lm1;
hence sup D = union D by A2, A1, YELLOW_0:def 9; :: thesis: verum