:: deftheorem defines axiom_GU3 CLASSES4:def 3 :
for GU being set holds
( GU is axiom_GU3 iff for x being set st x in GU holds
bool x in GU );