let A be non degenerated commutative Ring; :: thesis: for x being object holds
( x in Ideals A iff x is Ideal of A )
let x be object ; :: thesis: ( x in Ideals A iff x is Ideal of A )
thus ( x in Ideals A implies x is Ideal of A ) :: thesis: ( x is Ideal of A implies x in Ideals A )
proof
assume x in Ideals A ; :: thesis: x is Ideal of A
then x in { I where I is Ideal of A : verum } by RING_2:def 3;
then consider x0 being Ideal of A such that
A3: x0 = x ;
thus x is Ideal of A by A3; :: thesis: verum
end;
assume x is Ideal of A ; :: thesis: x in Ideals A
then x in { I where I is Ideal of A : verum } ;
hence x in Ideals A by RING_2:def 3; :: thesis: verum