let X, Y be set ; for M being with_empty_element Subset-Family of X
for N being with_empty_element Subset-Family of Y holds { [:A,B:] where A is Element of M, B is Element of N : verum } is with_empty_element Subset-Family of [:X,Y:]
let M be with_empty_element Subset-Family of X; for N being with_empty_element Subset-Family of Y holds { [:A,B:] where A is Element of M, B is Element of N : verum } is with_empty_element Subset-Family of [:X,Y:]
let N be with_empty_element Subset-Family of Y; { [:A,B:] where A is Element of M, B is Element of N : verum } is with_empty_element Subset-Family of [:X,Y:]
set L = { [:A,B:] where A is Element of M, B is Element of N : verum } ;
reconsider E1 = {} as Element of M by SETFAM_1:def 8;
reconsider E2 = {} as Element of N by SETFAM_1:def 8;
{} = [:E1,E2:]
by ZFMISC_1:90;
then
{} in { [:A,B:] where A is Element of M, B is Element of N : verum }
;
hence
{ [:A,B:] where A is Element of M, B is Element of N : verum } is with_empty_element Subset-Family of [:X,Y:]
by Th05; verum