now :: thesis: for m, n being odd Element of NAT st m <= len (W .reverse()) & n <= len (W .reverse()) & (W .reverse()) . m = (W .reverse()) . n holds
m = n

let m, n be odd Element of NAT ; :: thesis: ( m <= len (W .reverse()) & n <= len (W .reverse()) & (W .reverse()) . m = (W .reverse()) . n implies m = n )
assume A1: ( m <= len (W .reverse()) & n <= len (W .reverse()) ) ; :: thesis: ( (W .reverse()) . m = (W .reverse()) . n implies m = n )
( 1 <= m & 1 <= n ) by Th2;
then A2: ( m in dom (W .reverse()) & n in dom (W .reverse()) ) by A1, FINSEQ_3:25;
assume A3: (W .reverse()) . m = (W .reverse()) . n ; :: thesis: m = n
A4: ((len W) - m) + 1 in dom W by A2, GLIB_001:25;
then reconsider m9 = ((len W) - m) + 1 as odd Element of NAT ;
A5: m9 <= len W by A4, FINSEQ_3:25;
A6: ((len W) - n) + 1 in dom W by A2, GLIB_001:25;
then reconsider n9 = ((len W) - n) + 1 as odd Element of NAT ;
A7: n9 <= len W by A6, FINSEQ_3:25;
W . m9 = (W .reverse()) . m by A2, GLIB_001:25
.= W . n9 by A2, A3, GLIB_001:25 ;
then m9 = n9 by A5, A7, GLIB_001:def 29;
hence m = n ; :: thesis: verum

end;

hence W .reverse() is vertex-distinct ; :: thesis: verum