let a, b be ordinal number ; :: thesis: ( a in b & b in first_epsilon_greater_than a implies first_epsilon_greater_than b = first_epsilon_greater_than a )
assume Z0: ( a in b & b in first_epsilon_greater_than a ) ; :: thesis: first_epsilon_greater_than b = first_epsilon_greater_than a

now

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 Z0, ORDINAL1:19;
hence first_epsilon_greater_than a c= c by FEGT; :: thesis: verum

end;

hence first_epsilon_greater_than b = first_epsilon_greater_than a by Z0, FEGT; :: thesis: verum