let f be Denumeration of X; :: thesis: f is with_cardinal_domain
per cases ( X = {} or X <> {} ) ;
suppose X = {} ; :: thesis: f is with_cardinal_domain
hence f is with_cardinal_domain ; :: thesis: verum
end;
suppose X <> {} ; :: thesis: f is with_cardinal_domain
hence f is with_cardinal_domain ; :: thesis: verum
end;
end;