let X, x, y be set ; :: thesis: for f being Ordinal-Sequence st f = numbering X & x in dom f & y in dom f holds
( x c= y iff f . x c= f . y )
let f be Ordinal-Sequence; :: thesis: ( f = numbering X & x in dom f & y in dom f implies ( x c= y iff f . x c= f . y ) )
assume A1: ( f = numbering X & x in dom f & y in dom f ) ; :: thesis: ( x c= y iff f . x c= f . y )
then ( dom f = ord-type X & f is_isomorphism_of RelIncl (ord-type X), RelIncl (On X) ) by Th18, Th21;
hence ( x c= y iff f . x c= f . y ) by A1, Th6; :: thesis: verum