let L be non empty reflexive transitive RelStr ; :: thesis: for S being non empty full SubRelStr of L
for x being set st x in rng (idsMap S) holds
x is Ideal of L
let S be non empty full SubRelStr of L; :: thesis: for x being set st x in rng (idsMap S) holds
x is Ideal of L
let x be set ; :: thesis: ( x in rng (idsMap S) implies x is Ideal of L )
assume A1: x in rng (idsMap S) ; :: thesis: x is Ideal of L
rng (idsMap S) is Subset of (Ids L) by Th53;
then x in Ids L by A1;
then x in { X where X is Ideal of L : verum } by WAYBEL_0:def 23;
then ex I being Ideal of L st x = I ;
hence x is Ideal of L ; :: thesis: verum