let A, B be Ordinal; :: thesis: ( A in B iff Rank A in Rank B )
defpred S1[ Ordinal, Ordinal] means ( $1 in $2 implies Rank $1 in Rank $2 );
A1: now :: thesis: for A, B being Ordinal holds S2[B]
let A be Ordinal; :: thesis: for B being Ordinal holds S2[B]
defpred S2[ Ordinal] means S1[A,$1];
A2: for B being Ordinal st ( for C being Ordinal st C in B holds
S2[C] ) holds
S2[B]
proof
let B be Ordinal; :: thesis: ( ( for C being Ordinal st C in B holds
S2[C] ) implies S2[B] )
assume that
A3: for C being Ordinal st C in B holds
S1[A,C] and
A4: A in B ; :: thesis: Rank A in Rank B
A5: now :: thesis: ( ex C being Ordinal st B = succ C implies Rank A in Rank B )
given C being Ordinal such that A6: B = succ C ; :: thesis: Rank A in Rank B
A7: ( A in C implies Rank A in Rank C ) by A3, A6, ORDINAL1:6;
now :: thesis: ( not A in C implies Rank A = Rank C )
assume A8: not A in C ; :: thesis: Rank A = Rank C
( ( A c= C & A <> C ) iff A c< C ) ;
hence Rank A = Rank C by A4, A6, A8, ORDINAL1:11, ORDINAL1:22; :: thesis: verum
end;
then Rank A c= Rank C by A7, ORDINAL1:def 2;
hence Rank A in Rank B by A6, Th32; :: thesis: verum
end;
hence Rank A in Rank B by A5; :: thesis: verum
end;
thus for B being Ordinal holds S2[B] from ORDINAL1:sch 2(A2); :: thesis: verum
end;
hence S1[A,B] ; :: thesis: ( Rank A in Rank B implies A in B )
assume that
A13: Rank A in Rank B and
A14: not A in B ; :: thesis: contradiction
( B in A or B = A ) by A14, ORDINAL1:14;
hence contradiction by A1, A13; :: thesis: verum