[mizar] WELLFND1:1

[trybulec <trybulec@math.uwb.edu.pl>]

A comment in OSALG_1:

:: REVISE:: WELLFND1:1 should be generalised to Relation and moved to 
RELAT_1

The problem is that WELLFND1:1

theorem :: WELLFND1:1
 for X being set, f, g being Function st f c= g & X c= dom f holds f|X 
= g|X

is not true for Relations, e.g.

   f = { [1,2] }   g = {[1,2],[1,3]}  X = {1}

So, I have removed the comment.

Regards,
Andrzej