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 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