let R be domRing; :: thesis: for n being non empty Ordinal
for X, Y being Subset of (Funcs (n,([#] R))) st X c= Y holds
Ideal_ Y c= Ideal_ X
let n be non empty Ordinal; :: thesis: for X, Y being Subset of (Funcs (n,([#] R))) st X c= Y holds
Ideal_ Y c= Ideal_ X
let X, Y be Subset of (Funcs (n,([#] R))); :: thesis: ( X c= Y implies Ideal_ Y c= Ideal_ X )
assume A1: X c= Y ; :: thesis: Ideal_ Y c= Ideal_ X
for o being object st o in Ideal_ Y holds
o in Ideal_ X

proof

let o be object ; :: thesis: ( o in Ideal_ Y implies o in Ideal_ X )
assume o in Ideal_ Y ; :: thesis: o in Ideal_ X
then consider f being Polynomial of n,R such that
A3: ( f = o & Y c= Zero_ f ) ;
X c= Zero_ f by A3, A1;
hence o in Ideal_ X by A3; :: thesis: verum

end;

hence Ideal_ Y c= Ideal_ X ; :: thesis: verum