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 A2: X in Fin A ; :: thesis: X in Fin B
then X c= A by Def5;
then X c= B by A1, XBOOLE_1:1;
hence X in Fin B by A2, Def5; :: thesis: verum

end;

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