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 Th55;
hence contradiction by TARSKI:def 1; :: thesis: verum