:: deftheorem defines axiom_UP1 UNIFORM2:def 16 :
for X being set
for cB being Subset-Family of [:X,X:] holds
( cB is axiom_UP1 iff for B being Element of cB holds id X c= B );