assume not subset-closed_closure_of {} is empty ; :: thesis: contradiction
then consider x being object such that
A1: x in subset-closed_closure_of {} ;
reconsider x = x as set by TARSKI:1;
ex y being set st
( x c= y & y in {} ) by A1, Th2;
hence contradiction ; :: thesis: verum