let X, Y be set ; :: thesis: for f, g being PartFunc of X,Y st ( Y = {} implies X = {} ) & f tolerates g holds
TotFuncs f meets TotFuncs g
let f, g be PartFunc of X,Y; :: thesis: ( ( Y = {} implies X = {} ) & f tolerates g implies TotFuncs f meets TotFuncs g )
assume ( ( Y = {} implies X = {} ) & f tolerates g ) ; :: thesis: TotFuncs f meets TotFuncs g
then consider h being PartFunc of X,Y such that
A1: ( h is total & f tolerates h & g tolerates h ) by Th68;
( h in TotFuncs f & h in TotFuncs g ) by A1, Def5;
hence (TotFuncs f) /\ (TotFuncs g) <> {} by XBOOLE_0:def 4; :: according to XBOOLE_0:def 7 :: thesis: verum