let R be domRing; :: thesis: for n being non empty Ordinal
for X, Y being Algebraic_Set of n,R st X c< Y holds
Ideal_ Y c< Ideal_ X
let n be non empty Ordinal; :: thesis: for X, Y being Algebraic_Set of n,R st X c< Y holds
Ideal_ Y c< Ideal_ X
let X, Y be Algebraic_Set of n,R; :: thesis: ( X c< Y implies Ideal_ Y c< Ideal_ X )
assume A1: X c< Y ; :: thesis: Ideal_ Y c< Ideal_ X
Ideal_ X <> Ideal_ Y

proof

assume Ideal_ X = Ideal_ Y ; :: thesis: contradiction
then X = Zero_ (Ideal_ Y) by Th36
.= Y by Th36 ;
hence contradiction by A1; :: thesis: verum

end;

hence Ideal_ Y c< Ideal_ X by A1, Th29; :: thesis: verum