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

now

let X be set ; :: thesis: ( X in Fin A implies X in Fin B )
assume X in Fin A ; :: thesis: X in Fin B
then ( X c= A & X is finite ) by Def5;
then ( X c= B & X is finite ) by A1, XBOOLE_1:1;
hence X in Fin B by Def5; :: thesis: verum

end;

hence Fin A c= Fin B by TARSKI:def 3; :: thesis: verum