consider x being Subset of X such that
A1: x in S by SUBSET_1:4;
(x `) ` in S by A1;
hence not X \ S is empty by SETFAM_1:def 7; :: thesis: verum