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
set d = the Element of D;
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 object ; :: 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;
the Element of D in Ids R by A1;
then consider I being Ideal of R such that
A3: the Element of D = I and
verum ;
A4: 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;
A5: 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 that
A6: X in D and
A7: Y in D ; :: thesis: ex Z being Subset of R st
( Z in D & X \/ Y c= Z )

reconsider X1 = X, Y1 = Y as Element of (InclPoset (Ids R)) by A6, A7;
consider Z1 being Element of (InclPoset (Ids R)) such that
A8: Z1 in D and
A9: X1 <= Z1 and
A10: Y1 <= Z1 by ;
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
A11: Y1 c= Z1 by ;
X1 c= Z1 by ;
hence X \/ Y c= Z by ; :: thesis: verum
end;
A12: 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;
set i = the Element of I;
the Element of I in the Element of D by A3;
hence union D is Ideal of R by ; :: thesis: verum