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