let R be domRing; :: thesis: for n being non empty Ordinal
for S, T being Algebraic_Set of n,R holds S /\ T is Algebraic_Set of n,R
let n be non empty Ordinal; :: thesis: for S, T being Algebraic_Set of n,R holds S /\ T is Algebraic_Set of n,R
let S, T be Algebraic_Set of n,R; :: thesis: S /\ T is Algebraic_Set of n,R
consider I being Ideal of (Polynom-Ring (n,R)) such that
A1: S = Zero_ I by Def7;
consider J being Ideal of (Polynom-Ring (n,R)) such that
A2: T = Zero_ J by Def7;
reconsider Z = I \/ J as non empty Subset of (Polynom-Ring (n,R)) ;
reconsider M = Z -Ideal as Ideal of (Polynom-Ring (n,R)) ;
S /\ T = Zero_ (I \/ J) by A1, A2, Th18
.= Zero_ (Z -Ideal) by Th17 ;
then S /\ T is algebraic_set_from_ideal ;
hence S /\ T is Algebraic_Set of n,R ; :: thesis: verum