let X, Y be set ; :: thesis: 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; :: thesis: 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; :: thesis: { [: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; :: thesis: verum