set t = { (union A) where A is Subset-Family of [: the carrier of X, the carrier of Y:] : A c= { [:X1,Y1:] where X1 is Subset of X, Y1 is Subset of Y : ( X1 in the topology of X & Y1 in the topology of Y ) } } ;
{ (union A) where A is Subset-Family of [: the carrier of X, the carrier of Y:] : A c= { [:X1,Y1:] where X1 is Subset of X, Y1 is Subset of Y : ( X1 in the topology of X & Y1 in the topology of Y ) } } c= bool [: the carrier of X, the carrier of Y:]

let e be object ; :: according to TARSKI:def 3 :: thesis:
assume e in { (union A) where A is Subset-Family of [: the carrier of X, the carrier of Y:] : A c= { [:X1,Y1:] where X1 is Subset of X, Y1 is Subset of Y : ( X1 in the topology of X & Y1 in the topology of Y ) } } ; :: thesis:
then ex A being Subset-Family of [: the carrier of X, the carrier of Y:] st
( e = union A & A c= { [:X1,Y1:] where X1 is Subset of X, Y1 is Subset of Y : ( X1 in the topology of X & Y1 in the topology of Y ) } ) ;
hence e in bool [: the carrier of X, the carrier of Y:] ; :: thesis:

end;

then reconsider t = { (union A) where A is Subset-Family of [: the carrier of X, the carrier of Y:] : A c= { [:X1,Y1:] where X1 is Subset of X, Y1 is Subset of Y : ( X1 in the topology of X & Y1 in the topology of Y ) } } as Subset-Family of [: the carrier of X, the carrier of Y:] ;
set T = TopStruct(# [: the carrier of X, the carrier of Y:],t #);

now :: thesis:

reconsider A = {[: the carrier of X, the carrier of Y:]} as Subset-Family of [: the carrier of X, the carrier of Y:] by ZFMISC_1:68;
reconsider A = A as Subset-Family of [: the carrier of X, the carrier of Y:] ;
A1: A c= { [:X1,Y1:] where X1 is Subset of X, Y1 is Subset of Y : ( X1 in the topology of X & Y1 in the topology of Y ) }

proof

let e be object ; :: according to TARSKI:def 3 :: thesis:
assume e in A ; :: thesis:
then A2: e = [: the carrier of X, the carrier of Y:] by TARSKI:def 1;
( the carrier of X in the topology of X & the carrier of Y in the topology of Y ) by PRE_TOPC:def 1;
hence e in { [:X1,Y1:] where X1 is Subset of X, Y1 is Subset of Y : ( X1 in the topology of X & Y1 in the topology of Y ) } by A2; :: thesis:

end;

the carrier of TopStruct(# [: the carrier of X, the carrier of Y:],t #) = union A ;
hence the carrier of TopStruct(# [: the carrier of X, the carrier of Y:],t #) in the topology of TopStruct(# [: the carrier of X, the carrier of Y:],t #) by A1; :: thesis:
thus for a being Subset-Family of TopStruct(# [: the carrier of X, the carrier of Y:],t #) st a c= the topology of TopStruct(# [: the carrier of X, the carrier of Y:],t #) holds
union a in the topology of TopStruct(# [: the carrier of X, the carrier of Y:],t #) :: thesis:

proof

let a be Subset-Family of TopStruct(# [: the carrier of X, the carrier of Y:],t #); :: thesis:
set A = { [:X1,Y1:] where X1 is Subset of X, Y1 is Subset of Y : ( X1 in the topology of X & Y1 in the topology of Y & ex x being set st
( x in a & [:X1,Y1:] c= x ) ) } ;
{ [:X1,Y1:] where X1 is Subset of X, Y1 is Subset of Y : ( X1 in the topology of X & Y1 in the topology of Y & ex x being set st
( x in a & [:X1,Y1:] c= x ) ) } c= bool [: the carrier of X, the carrier of Y:]

proof

let e be object ; :: according to TARSKI:def 3 :: thesis:
assume e in { [:X1,Y1:] where X1 is Subset of X, Y1 is Subset of Y : ( X1 in the topology of X & Y1 in the topology of Y & ex x being set st
( x in a & [:X1,Y1:] c= x ) ) } ; :: thesis:
then ex X1 being Subset of X ex Y1 being Subset of Y st
( e = [:X1,Y1:] & X1 in the topology of X & Y1 in the topology of Y & ex x being set st
( x in a & [:X1,Y1:] c= x ) ) ;
hence e in bool [: the carrier of X, the carrier of Y:] ; :: thesis:

end;

then reconsider A = { [:X1,Y1:] where X1 is Subset of X, Y1 is Subset of Y : ( X1 in the topology of X & Y1 in the topology of Y & ex x being set st
( x in a & [:X1,Y1:] c= x ) ) } as Subset-Family of [: the carrier of X, the carrier of Y:] ;
assume A3: a c= the topology of TopStruct(# [: the carrier of X, the carrier of Y:],t #) ; :: thesis:
A4: union A = union a

proof

thus union A c= union a :: according to XBOOLE_0:def 10 :: thesis:

proof

let e1, e2 be object ; :: according to RELAT_1:def 3 :: thesis:
assume [e1,e2] in union A ; :: thesis:
then consider u being set such that
A5: [e1,e2] in u and
A6: u in A by TARSKI:def 4;
ex X1 being Subset of X ex Y1 being Subset of Y st
( u = [:X1,Y1:] & X1 in the topology of X & Y1 in the topology of Y & ex x being set st
( x in a & [:X1,Y1:] c= x ) ) by A6;
hence [e1,e2] in union a by A5, TARSKI:def 4; :: thesis:

end;

let e be object ; :: according to TARSKI:def 3 :: thesis:
assume e in union a ; :: thesis:
then consider u being set such that
A7: e in u and
A8: u in a by TARSKI:def 4;
u in the topology of TopStruct(# [: the carrier of X, the carrier of Y:],t #) by A3, A8;
then consider B being Subset-Family of [: the carrier of X, the carrier of Y:] such that
A9: u = union B and
A10: B c= { [:X1,Y1:] where X1 is Subset of X, Y1 is Subset of Y : ( X1 in the topology of X & Y1 in the topology of Y ) } ;
consider x being set such that
A11: e in x and
A12: x in B by A7, A9, TARSKI:def 4;
x in { [:X1,Y1:] where X1 is Subset of X, Y1 is Subset of Y : ( X1 in the topology of X & Y1 in the topology of Y ) } by A10, A12;
then consider X1 being Subset of X, Y1 being Subset of Y such that
A13: x = [:X1,Y1:] and
A14: ( X1 in the topology of X & Y1 in the topology of Y ) ;
[:X1,Y1:] c= u by A9, A12, A13, ZFMISC_1:74;
then x in A by A8, A13, A14;
hence e in union A by A11, TARSKI:def 4; :: thesis:

end;

A c= { [:X2,Y2:] where X2 is Subset of X, Y2 is Subset of Y : ( X2 in the topology of X & Y2 in the topology of Y ) }

proof

let e be object ; :: according to TARSKI:def 3 :: thesis:
assume e in A ; :: thesis:
then ex X1 being Subset of X ex Y1 being Subset of Y st
( e = [:X1,Y1:] & X1 in the topology of X & Y1 in the topology of Y & ex x being set st
( x in a & [:X1,Y1:] c= x ) ) ;
hence e in { [:X2,Y2:] where X2 is Subset of X, Y2 is Subset of Y : ( X2 in the topology of X & Y2 in the topology of Y ) } ; :: thesis:

end;

hence union a in the topology of TopStruct(# [: the carrier of X, the carrier of Y:],t #) by A4; :: thesis:

end;

let a, b be Subset of TopStruct(# [: the carrier of X, the carrier of Y:],t #); :: thesis:
set C = { [:X1,Y1:] where X1 is Subset of X, Y1 is Subset of Y : ( X1 in the topology of X & Y1 in the topology of Y & [:X1,Y1:] c= a /\ b ) } ;
{ [:X1,Y1:] where X1 is Subset of X, Y1 is Subset of Y : ( X1 in the topology of X & Y1 in the topology of Y & [:X1,Y1:] c= a /\ b ) } c= bool [: the carrier of X, the carrier of Y:]

proof

let e be object ; :: according to TARSKI:def 3 :: thesis:
assume e in { [:X1,Y1:] where X1 is Subset of X, Y1 is Subset of Y : ( X1 in the topology of X & Y1 in the topology of Y & [:X1,Y1:] c= a /\ b ) } ; :: thesis:
then ex X1 being Subset of X ex Y1 being Subset of Y st
( e = [:X1,Y1:] & X1 in the topology of X & Y1 in the topology of Y & [:X1,Y1:] c= a /\ b ) ;
hence e in bool [: the carrier of X, the carrier of Y:] ; :: thesis:

end;

then reconsider C = { [:X1,Y1:] where X1 is Subset of X, Y1 is Subset of Y : ( X1 in the topology of X & Y1 in the topology of Y & [:X1,Y1:] c= a /\ b ) } as Subset-Family of [: the carrier of X, the carrier of Y:] ;
assume that
A15: a in the topology of TopStruct(# [: the carrier of X, the carrier of Y:],t #) and
A16: b in the topology of TopStruct(# [: the carrier of X, the carrier of Y:],t #) ; :: thesis:
consider A being Subset-Family of [: the carrier of X, the carrier of Y:] such that
A17: a = union A and
A18: A c= { [:X1,Y1:] where X1 is Subset of X, Y1 is Subset of Y : ( X1 in the topology of X & Y1 in the topology of Y ) } by A15;
consider B being Subset-Family of [: the carrier of X, the carrier of Y:] such that
A19: b = union B and
A20: B c= { [:X1,Y1:] where X1 is Subset of X, Y1 is Subset of Y : ( X1 in the topology of X & Y1 in the topology of Y ) } by A16;
A21: a /\ b = union C

proof

thus a /\ b c= union C :: according to XBOOLE_0:def 10 :: thesis:

proof

let e be object ; :: according to TARSKI:def 3 :: thesis:
assume A22: e in a /\ b ; :: thesis:
then e in a by XBOOLE_0:def 4;
then consider u1 being set such that
A23: e in u1 and
A24: u1 in A by A17, TARSKI:def 4;
A25: u1 in { [:X1,Y1:] where X1 is Subset of X, Y1 is Subset of Y : ( X1 in the topology of X & Y1 in the topology of Y ) } by A18, A24;
e in b by A22, XBOOLE_0:def 4;
then consider u2 being set such that
A26: e in u2 and
A27: u2 in B by A19, TARSKI:def 4;
A28: u2 in { [:X2,Y2:] where X2 is Subset of X, Y2 is Subset of Y : ( X2 in the topology of X & Y2 in the topology of Y ) } by A20, A27;
A29: u2 c= b by A19, A27, ZFMISC_1:74;
consider X1 being Subset of X, Y1 being Subset of Y such that
A30: u1 = [:X1,Y1:] and
A31: ( X1 in the topology of X & Y1 in the topology of Y ) by A25;
consider X2 being Subset of X, Y2 being Subset of Y such that
A32: u2 = [:X2,Y2:] and
A33: ( X2 in the topology of X & Y2 in the topology of Y ) by A28;
u1 c= a by A17, A24, ZFMISC_1:74;
then [:X1,Y1:] /\ [:X2,Y2:] c= a /\ b by A30, A32, A29, XBOOLE_1:27;
then A34: [:(X1 /\ X2),(Y1 /\ Y2):] c= a /\ b by ZFMISC_1:100;
( X1 /\ X2 in the topology of X & Y1 /\ Y2 in the topology of Y ) by A31, A33, PRE_TOPC:def 1;
then A35: [:(X1 /\ X2),(Y1 /\ Y2):] in C by A34;
e in [:(X1 /\ X2),(Y1 /\ Y2):] by A23, A26, A30, A32, ZFMISC_1:113;
hence e in union C by A35, TARSKI:def 4; :: thesis:

end;

let e1, e2 be object ; :: according to RELAT_1:def 3 :: thesis:
assume [e1,e2] in union C ; :: thesis:
then consider u being set such that
A36: [e1,e2] in u and
A37: u in C by TARSKI:def 4;
ex X1 being Subset of X ex Y1 being Subset of Y st
( u = [:X1,Y1:] & X1 in the topology of X & Y1 in the topology of Y & [:X1,Y1:] c= a /\ b ) by A37;
hence [e1,e2] in a /\ b by A36; :: thesis:

end;

C c= { [:X1,Y1:] where X1 is Subset of X, Y1 is Subset of Y : ( X1 in the topology of X & Y1 in the topology of Y ) }

proof

let e be object ; :: according to TARSKI:def 3 :: thesis:
assume e in C ; :: thesis:
then ex X1 being Subset of X ex Y1 being Subset of Y st
( e = [:X1,Y1:] & X1 in the topology of X & Y1 in the topology of Y & [:X1,Y1:] c= a /\ b ) ;
hence e in { [:X1,Y1:] where X1 is Subset of X, Y1 is Subset of Y : ( X1 in the topology of X & Y1 in the topology of Y ) } ; :: thesis:

end;

hence a /\ b in the topology of TopStruct(# [: the carrier of X, the carrier of Y:],t #) by A21; :: thesis:

end;

then reconsider T = TopStruct(# [: the carrier of X, the carrier of Y:],t #) as strict TopSpace by PRE_TOPC:def 1;
take T ; :: thesis:
thus ( the carrier of T = [: the carrier of X, the carrier of Y:] & the topology of T = { (union A) where A is Subset-Family of T : A c= { [:X1,Y1:] where X1 is Subset of X, Y1 is Subset of Y : ( X1 in the topology of X & Y1 in the topology of Y ) } } ) ; :: thesis: