:: deftheorem defines axiom_GU1 CLASSES4:def 1 :
for GU being set holds
( GU is axiom_GU1 iff for x, y being set st x in GU & y in x holds
y in GU );