let a, b be ordinal number ; :: thesis: ( a c= b implies first_epsilon_greater_than a c= first_epsilon_greater_than b )
assume A0: a c= b ; :: thesis: first_epsilon_greater_than a c= first_epsilon_greater_than b
b in first_epsilon_greater_than b by FEGT;
then a in first_epsilon_greater_than b by A0, ORDINAL1:22;
hence first_epsilon_greater_than a c= first_epsilon_greater_than b by FEGT; :: thesis: verum