let UN be Universe; :: thesis: for X being Element of UN holds UN \ X is not Element of UN
let X be Element of UN; :: thesis: UN \ X is not Element of UN
not UN \ X in UN

proof

assume UN \ X in UN ; :: thesis: contradiction
then A1: (UN \ X) \/ X in UN by CLASSES2:60;
A2: (UN \ X) \/ X = UN \/ X by XBOOLE_1:39;
A3: UN \/ X c= UN

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in UN \/ X or x in UN )
assume x in UN \/ X ; :: thesis: x in UN
then ( x in UN or ( x in X & X in UN & UN is axiom_GU1 ) ) by XBOOLE_0:def 3;
hence x in UN ; :: thesis: verum

end;

UN = UN \/ X by A3, XBOOLE_1:7;
hence contradiction by A1, A2; :: thesis: verum

end;

hence UN \ X is not Element of UN ; :: thesis: verum