theorem Th34: :: NOMIN_1:34

for V, A being set
for m being Nat
for S being FinSequence
for D1, D2 being NonatomicND of V,A st D1 tolerates D2 & S IsNDRankSeq V,A & D1 in S . m & D2 in S . m holds
D1 \/ D2 in S . m