let A, B be Ordinal; :: thesis: ( ex C being Ordinal st
( C in A & not C in B ) implies for C being Ordinal st C in B holds
C in A )
given C being Ordinal such that A3: ( C in A & not C in B ) ; :: thesis: for C being Ordinal st C in B holds
C in A
let D be Ordinal; :: thesis: ( D in B implies D in A )
( A in B or A = B or B in A ) by Th10;
hence ( D in B implies D in A ) by A3, Th6; :: thesis: verum