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 in y iff f . x in f . y )
let f be Ordinal-Sequence; :: thesis: ( f = numbering X & x in dom f & y in dom f implies ( x in y iff f . x in f . y ) )
assume A1: ( f = numbering X & x in dom f & y in dom f ) ; :: thesis: ( x in y iff f . x in f . y )
then ( y c= x iff f . y c= f . x ) by Th22;
hence ( x in y iff f . x in f . y ) by A1, Th4; :: thesis: verum