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

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

ex Z being Subset of R st

( Z in D & X \/ Y c= Z )

X is lower

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

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

the Element of D in Ids R
by A1;
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;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

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

A5:
for X, Y being Subset of R st X in D & Y in D holds
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;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

ex Z being Subset of R st

( Z in D & X \/ Y c= Z )

proof

A12:
for X being Subset of R st X in D holds
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;( 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

X is lower

proof

set i = the Element of I;
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;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

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