let X be set ; :: thesis: for G1, G2 being Grothendieck of X holds G1 /\ G2 is Grothendieck of X

let G1, G2 be Grothendieck of X; :: thesis: G1 /\ G2 is Grothendieck of X

( X in G1 & X in G2 ) by Def4;

hence X in G1 /\ G2 by XBOOLE_0:def 4; :: according to CLASSES3:def 4 :: thesis: verum

let G1, G2 be Grothendieck of X; :: thesis: G1 /\ G2 is Grothendieck of X

( X in G1 & X in G2 ) by Def4;

hence X in G1 /\ G2 by XBOOLE_0:def 4; :: according to CLASSES3:def 4 :: thesis: verum