Re: If A=B & (A contains C), why mizar doesn't infer (B contains C)

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

On Mon, Jun 25, 2001 at 06:26:48PM +0200, Josef Urban wrote:

> There is practically no sense in having fictitious variables in loci (I
> can think of a very hypothetical case, when e.g. the type "Element of X"
> is needed, but we don't care at all about X (it is fictitious)).

I would like to see a real example for a need of ficticious arguments
besides for (how Andrzej puts it) creating fictitious theories.

The definitions in FUZZY_1 are really puzzling.  Does someone know why
they use 

	FuzzySet of C,h

instead of just

	Membership_Func of C

Maybe Grzegorz can ask his current boss.

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

I am a fundamentalist: always fun before mental.