let X1, X2 be set ; :: thesis: for A being Subset-Family of [:X1,X2:]
for A1 being non empty Subset-Family of X1
for A2 being non empty Subset-Family of X2 st A = { [:a,b:] where a is Subset of X1, b is Subset of X2 : ( a in A1 & b in A2 ) } holds
Intersect A = [:(Intersect A1),(Intersect A2):]
let A be Subset-Family of [:X1,X2:]; :: thesis: for A1 being non empty Subset-Family of X1
for A2 being non empty Subset-Family of X2 st A = { [:a,b:] where a is Subset of X1, b is Subset of X2 : ( a in A1 & b in A2 ) } holds
Intersect A = [:(Intersect A1),(Intersect A2):]
let A1 be non empty Subset-Family of X1; :: thesis: for A2 being non empty Subset-Family of X2 st A = { [:a,b:] where a is Subset of X1, b is Subset of X2 : ( a in A1 & b in A2 ) } holds
Intersect A = [:(Intersect A1),(Intersect A2):]
let A2 be non empty Subset-Family of X2; :: thesis: ( A = { [:a,b:] where a is Subset of X1, b is Subset of X2 : ( a in A1 & b in A2 ) } implies Intersect A = [:(Intersect A1),(Intersect A2):] )
assume A1: A = { [:a,b:] where a is Subset of X1, b is Subset of X2 : ( a in A1 & b in A2 ) } ; :: thesis: Intersect A = [:(Intersect A1),(Intersect A2):]

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: [:(Intersect A1),(Intersect A2):] c= Intersect A

let x be set ; :: thesis: ( x in Intersect A implies x in [:(Intersect A1),(Intersect A2):] )
assume A2: x in Intersect A ; :: thesis: x in [:(Intersect A1),(Intersect A2):]
then consider x1, x2 being set such that
A3: ( x1 in X1 & x2 in X2 & [x1,x2] = x ) by ZFMISC_1:def 2;
consider a1 being Element of A1, a2 being Element of A2;
reconsider a1 = a1 as Subset of X1 ;
reconsider a2 = a2 as Subset of X2 ;

now

let a be set ; :: thesis: ( a in A1 implies x1 in a )
assume a in A1 ; :: thesis: x1 in a
then [:a,a2:] in A by A1;
then x in [:a,a2:] by A2, SETFAM_1:58;
hence x1 in a by A3, ZFMISC_1:106; :: thesis: verum

end;

then A4: x1 in Intersect A1 by A3, SETFAM_1:58;

now

let a be set ; :: thesis: ( a in A2 implies x2 in a )
assume a in A2 ; :: thesis: x2 in a
then [:a1,a:] in A by A1;
then x in [:a1,a:] by A2, SETFAM_1:58;
hence x2 in a by A3, ZFMISC_1:106; :: thesis: verum

end;

then x2 in Intersect A2 by A3, SETFAM_1:58;
hence x in [:(Intersect A1),(Intersect A2):] by A3, A4, ZFMISC_1:106; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in [:(Intersect A1),(Intersect A2):] or x in Intersect A )
assume A5: x in [:(Intersect A1),(Intersect A2):] ; :: thesis: x in Intersect A
then consider x1, x2 being set such that
A6: ( x1 in Intersect A1 & x2 in Intersect A2 & [x1,x2] = x ) by ZFMISC_1:def 2;

now

let c be set ; :: thesis: ( c in A implies x in c )
assume c in A ; :: thesis: x in c
then consider a being Subset of X1, b being Subset of X2 such that
A7: ( c = [:a,b:] & a in A1 & b in A2 ) by A1;
( x1 in a & x2 in b ) by A6, A7, SETFAM_1:58;
hence x in c by A6, A7, ZFMISC_1:106; :: thesis: verum

end;

hence x in Intersect A by A5, SETFAM_1:58; :: thesis: verum