let a, b be Ordinal; :: thesis: ( a in b & b in first_epsilon_greater_than a implies first_epsilon_greater_than b = first_epsilon_greater_than a )
assume A1: ( a in b & b in first_epsilon_greater_than a ) ; :: thesis: first_epsilon_greater_than b = first_epsilon_greater_than a

now :: thesis: for c being epsilon Ordinal st b in c holds
first_epsilon_greater_than a c= c

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

end;

hence first_epsilon_greater_than b = first_epsilon_greater_than a by A1, Def6; :: thesis: verum