let Omega be non empty set ; :: thesis: for x, y being Subset of Omega st x misses y holds
x,y followed_by ({} Omega) is disjoint_valued
let x, y be Subset of Omega; :: thesis: ( x misses y implies x,y followed_by ({} Omega) is disjoint_valued )
assume A1: x misses y ; :: thesis: x,y followed_by ({} Omega) is disjoint_valued
reconsider r = x,y followed_by ({} Omega) as Function of NAT ,(bool Omega) ;

now

let n, m be Element of NAT ; :: thesis: ( n < m implies r . n misses r . m )
A2: ( m > 1 implies r . m = {} ) by FUNCT_7:126;
assume A3: n < m ; :: thesis: r . n misses r . m

A4: now

assume A5: ( m = 0 or m = 1 ) ; :: thesis: ( n = 0 & m = 1 )
0 + 1 = 1 ;
then n <= 0 by A3, A5, NAT_1:13;
hence ( n = 0 & m = 1 ) by A3, A5, NAT_1:3; :: thesis: verum

end;

r . 0 = x by FUNCT_7:124;
hence r . n misses r . m by A1, A4, A2, FUNCT_7:125, NAT_1:26, XBOOLE_1:65; :: thesis: verum

end;

hence x,y followed_by ({} Omega) is disjoint_valued by Def3; :: thesis: verum