per cases ( X = {} or X <> {} ) ;

suppose X = {} ; :: thesis: ex b₁ being a_partition of X st b₁ is finite

hence ex b₁ being a_partition of X st b₁ is finite by EQREL_1:45; :: thesis: verum

end;

suppose X <> {} ; :: thesis: ex b₁ being a_partition of X st b₁ is finite

then {X} is a_partition of X by EQREL_1:39;
hence ex b₁ being a_partition of X st b₁ is finite ; :: thesis: verum

end;

end;