let M be ManySortedSet of I; :: thesis: ( M is V3() implies M is disjoint_valued )
assume A1: M is V3() ; :: thesis: M is disjoint_valued
let x, y be object ; :: according to PROB_2:def 2 :: thesis: ( x = y or M . x misses M . y )
assume x <> y ; :: thesis: M . x misses M . y
per cases ( ( x in dom M & y in dom M ) or not x in dom M or not y in dom M ) ;
suppose ( x in dom M & y in dom M ) ; :: thesis: M . x misses M . y
M . x is empty by A1;
hence M . x misses M . y by XBOOLE_1:65; :: thesis: verum
end;
suppose ( not x in dom M or not y in dom M ) ; :: thesis: M . x misses M . y
then ( M . x = {} or M . y = {} ) by FUNCT_1:def 2;
hence M . x misses M . y by XBOOLE_1:65; :: thesis: verum
end;
end;