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 )
set h = the Element of (TotFuncs f) /\ (TotFuncs g);
assume A1: (TotFuncs f) /\ (TotFuncs g) <> {} ; :: according to XBOOLE_0:def 7 :: thesis: f tolerates g
then A2: the Element of (TotFuncs f) /\ (TotFuncs g) in TotFuncs f by XBOOLE_0:def 4;
A3: the Element of (TotFuncs f) /\ (TotFuncs g) in TotFuncs g by A1, XBOOLE_0:def 4;
reconsider h = the Element of (TotFuncs f) /\ (TotFuncs g) as PartFunc of X,Y by A2, Th69;
A4: g tolerates h by A3, Th71;
f tolerates h by A2, Th71;
hence f tolerates g by A2, A4, Th67, Th70; :: thesis: verum