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

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