reconsider R = {} as Rule ;
take R ; :: thesis: ( dom R c= Fin Fml & rng R c= Fml )
thus ( dom R c= Fin Fml & rng R c= Fml ) ; :: thesis: verum