{} c= X by XBOOLE_1:2;
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