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