{} c= X ;
then reconsider R = {[{},{}]} as Relation of (bool X) by RELSET_1:3;
take R ; :: thesis: ( not R is empty & R is finite )
thus not R is empty ; :: thesis: R is finite
thus R is finite ; :: thesis: verum