set X = {{}};
reconsider R = {} as Rule ;
( dom R c= Fin {{}} & rng R c= {{}} ) ;
then reconsider R = R as Rule of {{}} by Def2;
take ProofSystem(# {{}},([#] {{}}),R #) ; :: thesis: not ProofSystem(# {{}},([#] {{}}),R #) is empty
thus not ProofSystem(# {{}},([#] {{}}),R #) is empty ; :: thesis: verum