let L be sup-Semilattice; :: thesis: for X being non empty lower Subset of L holds

( X is Ideal of L iff subrelstr X is join-inheriting )

let X be non empty lower Subset of L; :: thesis: ( X is Ideal of L iff subrelstr X is join-inheriting )

set S = subrelstr X;

A1: the carrier of (subrelstr X) = X by YELLOW_0:def 15;

sup {x,y} in the carrier of (subrelstr X) ; :: according to YELLOW_0:def 17 :: thesis: X is Ideal of L

X is directed

( X is Ideal of L iff subrelstr X is join-inheriting )

let X be non empty lower Subset of L; :: thesis: ( X is Ideal of L iff subrelstr X is join-inheriting )

set S = subrelstr X;

A1: the carrier of (subrelstr X) = X by YELLOW_0:def 15;

hereby :: thesis: ( subrelstr X is join-inheriting implies X is Ideal of L )

assume A9:
for x, y being Element of L st x in the carrier of (subrelstr X) & y in the carrier of (subrelstr X) & ex_sup_of {x,y},L holds assume A2:
X is Ideal of L
; :: thesis: subrelstr X is join-inheriting

thus subrelstr X is join-inheriting :: thesis: verum

end;thus subrelstr X is join-inheriting :: thesis: verum

proof

let x, y be Element of L; :: according to YELLOW_0:def 17 :: thesis: ( not x in the carrier of (subrelstr X) or not y in the carrier of (subrelstr X) or not ex_sup_of {x,y},L or "\/" ({x,y},L) in the carrier of (subrelstr X) )

assume that

A3: x in the carrier of (subrelstr X) and

A4: y in the carrier of (subrelstr X) and

A5: ex_sup_of {x,y},L ; :: thesis: "\/" ({x,y},L) in the carrier of (subrelstr X)

consider z being Element of L such that

A6: z in X and

A7: x <= z and

A8: y <= z by A1, A2, A3, A4, Def1;

z is_>=_than {x,y} by A7, A8, YELLOW_0:8;

then z >= sup {x,y} by A5, YELLOW_0:def 9;

hence "\/" ({x,y},L) in the carrier of (subrelstr X) by A1, A6, Def19; :: thesis: verum

end;assume that

A3: x in the carrier of (subrelstr X) and

A4: y in the carrier of (subrelstr X) and

A5: ex_sup_of {x,y},L ; :: thesis: "\/" ({x,y},L) in the carrier of (subrelstr X)

consider z being Element of L such that

A6: z in X and

A7: x <= z and

A8: y <= z by A1, A2, A3, A4, Def1;

z is_>=_than {x,y} by A7, A8, YELLOW_0:8;

then z >= sup {x,y} by A5, YELLOW_0:def 9;

hence "\/" ({x,y},L) in the carrier of (subrelstr X) by A1, A6, Def19; :: thesis: verum

sup {x,y} in the carrier of (subrelstr X) ; :: according to YELLOW_0:def 17 :: thesis: X is Ideal of L

X is directed

proof

hence
X is Ideal of L
; :: thesis: verum
let x, y be Element of L; :: according to WAYBEL_0:def 1 :: thesis: ( x in X & y in X implies ex z being Element of L st

( z in X & x <= z & y <= z ) )

assume that

A10: x in X and

A11: y in X ; :: thesis: ex z being Element of L st

( z in X & x <= z & y <= z )

take z = sup {x,y}; :: thesis: ( z in X & x <= z & y <= z )

A12: z = x "\/" y by YELLOW_0:41;

ex_sup_of {x,y},L by YELLOW_0:20;

hence ( z in X & x <= z & y <= z ) by A1, A9, A10, A11, A12, YELLOW_0:18; :: thesis: verum

end;( z in X & x <= z & y <= z ) )

assume that

A10: x in X and

A11: y in X ; :: thesis: ex z being Element of L st

( z in X & x <= z & y <= z )

take z = sup {x,y}; :: thesis: ( z in X & x <= z & y <= z )

A12: z = x "\/" y by YELLOW_0:41;

ex_sup_of {x,y},L by YELLOW_0:20;

hence ( z in X & x <= z & y <= z ) by A1, A9, A10, A11, A12, YELLOW_0:18; :: thesis: verum