[mizar] Was this supposed to be so?

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

Hi:

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