let R be domRing; :: thesis: for n being non empty Ordinal
for V, W being Algebraic_Set of n,R holds
( V = W iff Ideal_ V = Ideal_ W )
let n be non empty Ordinal; :: thesis: for V, W being Algebraic_Set of n,R holds
( V = W iff Ideal_ V = Ideal_ W )
let V, W be Algebraic_Set of n,R; :: thesis: ( V = W iff Ideal_ V = Ideal_ W )
( Ideal_ V = Ideal_ W implies V = W )

proof

assume Ideal_ V = Ideal_ W ; :: thesis: V = W
then V = Zero_ (Ideal_ W) by Th36
.= W by Th36 ;
hence V = W ; :: thesis: verum

end;

hence ( V = W iff Ideal_ V = Ideal_ W ) ; :: thesis: verum