let A, B be set ; :: thesis: ( ( for x, y being set st x in A & y in B holds
x misses y ) implies union A misses union B )
assume A1: for x, y being set st x in A & y in B holds
x misses y ; :: thesis: union A misses union B
for y being set st y in B holds
union A misses y
proof
let y be set ; :: thesis: ( y in B implies union A misses y )
assume y in B ; :: thesis: union A misses y
then for x being set st x in A holds
x misses y by A1;
hence union A misses y by Th79; :: thesis: verum
end;
hence union A misses union B by Th79; :: thesis: verum