Dear Andrzej,
>A proof starting with
> let X be empty infinite set
>looks pretty nice.
Actually I think it looks funny :-)
But what if someone starts a proof with
let X be set such that X is empty infinite;
Why not forbid that also? Maybe we should require people for
each "let x such that A" to prove that "ex x st A" (correctness
condition for "let" :-))
Freek