let V, A be set ; :: thesis: 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; :: thesis: ( D1 tolerates D2 implies D1 \/ D2 is NonatomicND of V,A )

set D = D1 \/ D2;

assume A1: D1 tolerates D2 ; :: thesis: 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; :: thesis: verum

D1 \/ D2 is NonatomicND of V,A

let D1, D2 be NonatomicND of V,A; :: thesis: ( D1 tolerates D2 implies D1 \/ D2 is NonatomicND of V,A )

set D = D1 \/ D2;

assume A1: D1 tolerates D2 ; :: thesis: 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; :: thesis: verum