:: deftheorem Def1 defines standard-ins COMPOS_0:def 1 :
for S being set holds
( S is standard-ins iff ex X being non empty set st S c= [:NAT,(NAT *),(X *):] );