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 A6, 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
A11: Y1 c= Z1 by A10, YELLOW_1:3;
X1 c= Z1 by A9, YELLOW_1:3;
hence X \/ Y c= Z by A11, XBOOLE_1:8; :: 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 A12, A2, A4, A5, TARSKI:def 4, WAYBEL_0:26, WAYBEL_0:46; :: thesis: verum