:: deftheorem defines axiom_GU2 CLASSES4:def 2 :
for GU being set holds
( GU is axiom_GU2 iff for x, y being set st x in GU & y in GU holds
{x,y} in GU );