let p, q be Function; :: thesis: ( q is disjoint_valued & p c= q implies p is disjoint_valued )
assume A1: ( q is disjoint_valued & p c= q ) ; :: thesis: p is disjoint_valued
for x, y being set st x <> y holds
p . x misses p . y

proof

let x, y be set ; :: thesis: ( x <> y implies p . x misses p . y )
assume A2: x <> y ; :: thesis: p . x misses p . y
assume A3: p . x meets p . y ; :: thesis: contradiction
( x in dom p & y in dom p )

proof

assume ( not x in dom p or not y in dom p ) ; :: thesis: contradiction
then ( p . x = {} or p . y = {} ) by FUNCT_1:def 4;
hence contradiction by A3, XBOOLE_1:65; :: thesis: verum

end;

then ( p . x = q . x & p . y = q . y ) by A1, GRFUNC_1:8;
hence contradiction by A1, A2, A3, PROB_2:def 3; :: thesis: verum

end;

hence p is disjoint_valued by PROB_2:def 3; :: thesis: verum