let V, A be set ; for S1, S2 being FinSequence st S1 IsNDRankSeq V,A & S2 IsNDRankSeq V,A & not S1 c= S2 holds
S2 c= S1
let S1, S2 be FinSequence; ( S1 IsNDRankSeq V,A & S2 IsNDRankSeq V,A & not S1 c= S2 implies S2 c= S1 )
assume
( S1 IsNDRankSeq V,A & S2 IsNDRankSeq V,A )
; ( S1 c= S2 or S2 c= S1 )
then A1:
( S1 = (FNDSC (V,A)) | (dom S1) & S2 = (FNDSC (V,A)) | (dom S2) )
by Th20;
( dom S1 c= dom S2 or dom S2 c= dom S1 )
by Th3;
hence
( S1 c= S2 or S2 c= S1 )
by A1, RELAT_1:75; verum