let x be set ; :: according to FINSET_1:def 6 :: thesis: ( not x in subset-closed_closure_of X or x is finite )
assume x in subset-closed_closure_of X ; :: thesis: x is finite
then consider y being set such that
A1: x c= y and
A2: y in X by Th2;
y is finite by A2;
hence x is finite by A1; :: thesis: verum