let X1, X2 be set ; :: thesis: for S1 being non empty Subset-Family of X1
for S2 being non empty Subset-Family of X2 holds { [:a,b:] where a is Element of S1, b is Element of S2 : verum } is non empty Subset-Family of [:X1,X2:]
let S1 be non empty Subset-Family of X1; :: thesis: for S2 being non empty Subset-Family of X2 holds { [:a,b:] where a is Element of S1, b is Element of S2 : verum } is non empty Subset-Family of [:X1,X2:]
let S2 be non empty Subset-Family of X2; :: thesis: { [:a,b:] where a is Element of S1, b is Element of S2 : verum } is non empty Subset-Family of [:X1,X2:]
set L = { [:a,b:] where a is Element of S1, b is Element of S2 : verum } ;
A1: { [:a,b:] where a is Element of S1, b is Element of S2 : verum } = { s where s is Subset of [:X1,X2:] : ex x1, x2 being set st
( x1 in S1 & x2 in S2 & s = [:x1,x2:] ) } by SRINGS_2:2;
consider a being object such that
A2: a in S1 by XBOOLE_0:def 1;
consider b being object such that
A3: b in S2 by XBOOLE_0:def 1;
reconsider a = a as Element of S1 by A2;
reconsider b = b as Element of S2 by A3;
A4: [:a,b:] in { [:a,b:] where a is Element of S1, b is Element of S2 : verum } ;

now :: thesis: for z being object st z in { [:a,b:] where a is Element of S1, b is Element of S2 : verum } holds
z in bool [:X1,X2:]

let z be object ; :: thesis: ( z in { [:a,b:] where a is Element of S1, b is Element of S2 : verum } implies z in bool [:X1,X2:] )
assume z in { [:a,b:] where a is Element of S1, b is Element of S2 : verum } ; :: thesis: z in bool [:X1,X2:]
then ex s being Subset of [:X1,X2:] st
( z = s & ex x1, x2 being set st
( x1 in S1 & x2 in S2 & s = [:x1,x2:] ) ) by A1;
hence z in bool [:X1,X2:] ; :: thesis: verum

end;

then { [:a,b:] where a is Element of S1, b is Element of S2 : verum } c= bool [:X1,X2:] ;
hence { [:a,b:] where a is Element of S1, b is Element of S2 : verum } is non empty Subset-Family of [:X1,X2:] by A4; :: thesis: verum