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