let X be finite subset-closed set ; :: thesis: Sub_of_Fin X = X
thus Sub_of_Fin X c= X ; :: according to XBOOLE_0:def 10 :: thesis: X c= Sub_of_Fin X
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in X or x in Sub_of_Fin X )
reconsider xx = x as set by TARSKI:1;
assume A1: x in X ; :: thesis: x in Sub_of_Fin X
bool xx c= X by A1, CLASSES1:def 1;
then xx is finite ;
hence x in Sub_of_Fin X by A1, Def3; :: thesis: verum