:: deftheorem defines axiom_UP2 UNIFORM3:def 1 :
for X being set
for cB being Subset-Family of [:X,X:] holds
( cB is axiom_UP2 iff for B1 being Element of cB ex B2 being Element of cB st B2 c= B1 ~ );