let X be non empty set ; :: thesis: for GX being Grothendieck of X
for G being Universe st X misses G holds
GX <> G
let GX be Grothendieck of X; :: thesis: for G being Universe st X misses G holds
GX <> G
let G be Universe; :: thesis: ( X misses G implies GX <> G )
assume A1: X misses G ; :: thesis: GX <> G
assume GX = G ; :: thesis: contradiction
then ( X in G & G is axiom_GU1 & G is axiom_GU3 ) by CLASSES3:def 4;
then X c= G ;
hence contradiction by A1, XBOOLE_1:68; :: thesis: verum