let V, A be set ; for D1, D2 being NonatomicND of V,A st D1 tolerates D2 holds
D1 \/ D2 is NonatomicND of V,A
let D1, D2 be NonatomicND of V,A; ( D1 tolerates D2 implies D1 \/ D2 is NonatomicND of V,A )
set D = D1 \/ D2;
assume A1:
D1 tolerates D2
; D1 \/ D2 is NonatomicND of V,A
then A2:
D1 \/ D2 is Function
by PARTFUN1:51;
consider S1 being FinSequence such that
A3:
S1 IsNDRankSeq V,A
and
A4:
D1 in Union S1
by Def5;
consider S2 being FinSequence such that
A5:
S2 IsNDRankSeq V,A
and
A6:
D2 in Union S2
by Def5;
( S1 c= S2 or S2 c= S1 )
by A3, A5, Th22;
hence
D1 \/ D2 is NonatomicND of V,A
by A1, A2, A3, A4, A5, A6, Th35, Def5; verum