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 set ; :: according to TARSKI:def 3 :: thesis: ( not x in X or x in Sub_of_Fin X )
assume A1: x in X ; :: thesis: x in Sub_of_Fin X
bool x c= X

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in bool x or y in X )
assume y in bool x ; :: thesis: y in X
hence y in X by A1, CLASSES1:def 1; :: thesis: verum

end;

then x is finite ;
hence x in Sub_of_Fin X by A1, Def3; :: thesis: verum