for Y, Z being set st Y in {} & Z in {} holds
( [Y,Z] in {} iff Y c= Z ) ;
hence RelIncl {} is empty by RELAT_1:63, Def1; :: thesis: verum