let U be Universe; :: thesis: for x being object holds
( x in U iff {x} in U )
let x be object ; :: thesis: ( x in U iff {x} in U )
thus ( x in U implies {x} in U ) by CLASSES2:57; :: thesis: ( {x} in U implies x in U )
assume {x} in U ; :: thesis: x in U
then ( x in {x} & {x} in U ) by TARSKI:def 1;
hence x in U by CLASSES4:def 1; :: thesis: verum