let R be non empty reflexive transitive RelStr ; :: thesis: for D being non empty directed Subset of (InclPoset (Ids R)) holds union D is Ideal of R
let D be non empty directed Subset of (InclPoset (Ids R)); :: thesis: union D is Ideal of R
D c= the carrier of (InclPoset (Ids R)) ;
then A1: D c= Ids R by YELLOW_1:1;
A2: D c= bool the carrier of R

proof

let d be set ; :: according to TARSKI:def 3 :: thesis: ( not d in D or d in bool the carrier of R )
assume d in D ; :: thesis: d in bool the carrier of R
then d in Ids R by A1;
then ex I being Ideal of R st d = I ;
hence d in bool the carrier of R ; :: thesis: verum

end;

consider d being Element of D;
d in D ;
then d in Ids R by A1;
then consider I being Ideal of R such that
A3: d = I and
verum ;
consider i being Element of I;
A4: i in d by A3;
A5: for X being Subset of R st X in D holds
X is directed

proof

let X be Subset of R; :: thesis: ( X in D implies X is directed )
assume X in D ; :: thesis: X is directed
then X in Ids R by A1;
then ex I being Ideal of R st X = I ;
hence X is directed ; :: thesis: verum

end;

A6: for X, Y being Subset of R st X in D & Y in D holds
ex Z being Subset of R st
( Z in D & X \/ Y c= Z )

proof

let X, Y be Subset of R; :: thesis: ( X in D & Y in D implies ex Z being Subset of R st
( Z in D & X \/ Y c= Z ) )
assume A7: ( X in D & Y in D ) ; :: thesis: ex Z being Subset of R st
( Z in D & X \/ Y c= Z )
then reconsider X1 = X, Y1 = Y as Element of (InclPoset (Ids R)) ;
consider Z1 being Element of (InclPoset (Ids R)) such that
A8: ( Z1 in D & X1 <= Z1 & Y1 <= Z1 ) by A7, WAYBEL_0:def 1;
Z1 in Ids R by A1, A8;
then ex I being Ideal of R st Z1 = I ;
then reconsider Z = Z1 as Subset of R ;
take Z ; :: thesis: ( Z in D & X \/ Y c= Z )
thus Z in D by A8; :: thesis: X \/ Y c= Z
( X1 c= Z1 & Y1 c= Z1 ) by A8, YELLOW_1:3;
hence X \/ Y c= Z by XBOOLE_1:8; :: thesis: verum

end;

for X being Subset of R st X in D holds
X is lower

proof

let X be Subset of R; :: thesis: ( X in D implies X is lower )
assume X in D ; :: thesis: X is lower
then X in Ids R by A1;
then ex I being Ideal of R st X = I ;
hence X is lower ; :: thesis: verum

end;

hence union D is Ideal of R by A2, A4, A5, A6, TARSKI:def 4, WAYBEL_0:26, WAYBEL_0:46; :: thesis: verum