let L be lower-bounded continuous sup-Semilattice; :: thesis: for B being with_bottom CLbasis of L

for x being set st x in rng (baseMap B) holds

x is Ideal of (subrelstr B)

let B be with_bottom CLbasis of L; :: thesis: for x being set st x in rng (baseMap B) holds

x is Ideal of (subrelstr B)

let x be set ; :: thesis: ( x in rng (baseMap B) implies x is Ideal of (subrelstr B) )

A1: rng (baseMap B) is Subset of (Ids (subrelstr B)) by YELLOW_1:1;

assume x in rng (baseMap B) ; :: thesis: x is Ideal of (subrelstr B)

then x in Ids (subrelstr B) by A1;

then x in { X where X is Ideal of (subrelstr B) : verum } by WAYBEL_0:def 23;

then ex I being Ideal of (subrelstr B) st x = I ;

hence x is Ideal of (subrelstr B) ; :: thesis: verum

for x being set st x in rng (baseMap B) holds

x is Ideal of (subrelstr B)

let B be with_bottom CLbasis of L; :: thesis: for x being set st x in rng (baseMap B) holds

x is Ideal of (subrelstr B)

let x be set ; :: thesis: ( x in rng (baseMap B) implies x is Ideal of (subrelstr B) )

A1: rng (baseMap B) is Subset of (Ids (subrelstr B)) by YELLOW_1:1;

assume x in rng (baseMap B) ; :: thesis: x is Ideal of (subrelstr B)

then x in Ids (subrelstr B) by A1;

then x in { X where X is Ideal of (subrelstr B) : verum } by WAYBEL_0:def 23;

then ex I being Ideal of (subrelstr B) st x = I ;

hence x is Ideal of (subrelstr B) ; :: thesis: verum