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