take U ; :: thesis: U is U -Class
U c= U ;
then ( U in bool U & not U in U ) ;
hence U is U -Class ; :: thesis: verum