:: deftheorem defines axiom_UP3 UNIFORM2:def 17 :
for X being set
for cB being Subset-Family of [:X,X:] holds
( cB is axiom_UP3 iff for B1 being Element of cB ex B2 being Element of cB st B2 [*] B2 c= B1 );