let V, A be set ; :: thesis: 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; :: thesis: ( 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 ) ; :: thesis: ( 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; :: thesis: verum