let a, b be Ordinal; :: thesis: ( a c= b implies first_epsilon_greater_than a c= first_epsilon_greater_than b )
assume A1: a c= b ; :: thesis: first_epsilon_greater_than a c= first_epsilon_greater_than b
b in first_epsilon_greater_than b by Def6;
then a in first_epsilon_greater_than b by A1, ORDINAL1:12;
hence first_epsilon_greater_than a c= first_epsilon_greater_than b by Def6; :: thesis: verum