let A, B be set ; :: thesis: ( A c= B implies Fin A c= Fin B )
assume A1: A c= B ; :: thesis: Fin A c= Fin B
let X be object ; :: according to TARSKI:def 3 :: thesis: ( not X in Fin A or X in Fin B )
reconsider XX = X as set by TARSKI:1;
assume A2: X in Fin A ; :: thesis: X in Fin B
then XX c= A by Def5;
then XX c= B by A1;
hence X in Fin B by A2, Def5; :: thesis: verum