( union {{} } = {} & Total {} = {} ) by ZFMISC_1:31;
hence Web {{} } = {} ; :: thesis: verum