reconsider IT = {} null S as Subset of X by XBOOLE_1:2;
take IT ; :: thesis: IT is S -correct
thus IT is S -correct ; :: thesis: verum