let UN be Universe; :: thesis: { u where u is Element of UN : verum } is not Element of UN
set SETUN = { u where u is Element of UN : verum } ;
assume A1: { u where u is Element of UN : verum } is Element of UN ; :: thesis: contradiction

now :: thesis: ( { u where u is Element of UN : verum } c= UN & UN c= { u where u is Element of UN : verum } )

thus { u where u is Element of UN : verum } c= UN :: thesis: UN c= { u where u is Element of UN : verum }

proof

let o be object ; :: according to TARSKI:def 3 :: thesis: ( not o in { u where u is Element of UN : verum } or o in UN )
assume o in { u where u is Element of UN : verum } ; :: thesis: o in UN
then ex u being Element of UN st o = u ;
hence o in UN ; :: thesis: verum

end;

thus UN c= { u where u is Element of UN : verum } ; :: thesis: verum

end;

then { u where u is Element of UN : verum } = UN ;
then UN in UN by A1;
hence contradiction ; :: thesis: verum