Re: [mizar] Was this supposed to be so?

[Piotr Rudnicki <piotr@cs.ualberta.ca>]

Hi:

I appreciate Grzegorz's, as always deep and careful, explanation but
I expected an error that the skeleton of the proof disagrees with the
thesis.


On Tue, Aug 20, 2002 at 02:07:53PM -0600, Piotr Rudnicki wrote:
> 
> I have expected an error in the following
> 
> 	for X, Y, Z being set st X = Y holds Y = X
> 	proof let X, Y be set;
> 	  thus thesis;
> 	end;
> 
> but did not get any.  Such theorem would look pretty silly in an abstract.

-- 
Piotr Rudnicki              CompSci, University of Alberta, Edmonton, Canada
email: piotr@cs.ualberta.ca                 http://web.cs.ualberta.ca/~piotr