let U be Universe; :: thesis: for X being Set of U holds U \ X is class of U
let X be Set of U; :: thesis: U \ X is class of U
A1: X is U -set by Def10;

now :: thesis: not U \ X = {}

assume U \ X = {} ; :: thesis: contradiction
then U c= X by XBOOLE_1:37;
then X in X by A1;
hence contradiction ; :: thesis: verum

end;

then reconsider UX = U \ X as non empty set ;
X is U -set by Def10;
then ( U \ X c= U & not U \ X in U ) by XBOOLE_1:36, CLASSES4:86;
then UX is U -Class ;
hence U \ X is class of U by Def12; :: thesis: verum