thus ( A c= B implies for C being Ordinal st C in A holds
C in B ) ; :: thesis: ( ( for C being Ordinal st C in A holds
C in B ) implies A c= B )
assume A1: for C being Ordinal st C in A holds
C in B ; :: thesis: A c= B
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in A or x in B )
assume A2: x in A ; :: thesis: x in B
then reconsider C = x as Ordinal by Th9;
C in B by A1, A2;
hence x in B ; :: thesis: verum