let X, Y be set ; :: thesis: for f, g being PartFunc of X,Y st TotFuncs f meets TotFuncs g holds
f tolerates g
let f, g be PartFunc of X,Y; :: thesis: ( TotFuncs f meets TotFuncs g implies f tolerates g )
consider h being Element of (TotFuncs f) /\ (TotFuncs g);
assume A1: (TotFuncs f) /\ (TotFuncs g) <> {} ; :: according to XBOOLE_0:def 7 :: thesis: f tolerates g
then A2: h in TotFuncs f by XBOOLE_0:def 4;
A3: h in TotFuncs g by A1, XBOOLE_0:def 4;
reconsider h = h as PartFunc of X,Y by A2, Th168;
A4: g tolerates h by A3, Th171;
f tolerates h by A2, Th171;
hence f tolerates g by A2, A4, Th158, Th169; :: thesis: verum