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 )
assume A1: (TotFuncs f) /\ (TotFuncs g) <> {} ; :: according to XBOOLE_0:def 7 :: thesis: f tolerates g
consider h being Element of (TotFuncs f) /\ (TotFuncs g);
A2: ( h in TotFuncs f & h in TotFuncs g ) by A1, XBOOLE_0:def 4;
then reconsider h = h as PartFunc of X,Y by Th168;
( h is total & f tolerates h & g tolerates h ) by A2, Th169, Th171;
hence f tolerates g by Th158; :: thesis: verum