per cases ( X = {} or X <> {} ) ;
suppose X = {} ; :: thesis: ex b1 being a_partition of X st b1 is finite
hence ex b1 being a_partition of X st b1 is finite by EQREL_1:45; :: thesis: verum
end;
suppose X <> {} ; :: thesis: ex b1 being a_partition of X st b1 is finite
then {X} is a_partition of X by EQREL_1:39;
hence ex b1 being a_partition of X st b1 is finite ; :: thesis: verum
end;
end;