take <*{{}}*> ; :: thesis: ( not <*{{}}*> is empty & <*{{}}*> is non-empty )
thus not <*{{}}*> is empty ; :: thesis: <*{{}}*> is non-empty
assume {} in rng <*{{}}*> ; :: according to RELAT_1:def 9 :: thesis: contradiction
then {} in {{{}}} by Th38;
hence contradiction by TARSKI:def 1; :: thesis: verum