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

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