for X being non empty set
for S being SigmaField of X
for E1, E2 being Element of S st E1 misses E2 holds
<*E1,E2*> is Finite_Sep_Sequence of S