:: deftheorem defines @ AOFA_L00:def 15 :
for I being non empty set
for X being V2() ManySortedSet of I
for S being V2() ManySortedSubset of X
for x being Element of I
for z being Element of S . x holds @ z = z;