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

proof

let x, y be object ; :: thesis: ( x <> y implies p . x misses p . y )
assume A3: x <> y ; :: thesis: p . x misses p . y
assume A4: 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 2;
hence contradiction by A4; :: thesis: verum

end;

then ( p . x = q . x & p . y = q . y ) by A2, GRFUNC_1:2;
hence contradiction by A1, A3, A4; :: thesis: verum

end;

hence p is disjoint_valued ; :: thesis: verum