theorem :: CLASSES4:6

for G being non empty set st G is axiom_GU1 & G is axiom_GU2 & G is axiom_GU3 & G is axiom_GU4 holds
G is non empty Grothendieck by Th3, Th4, CLASSES3:def 1;