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

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