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:]

set T = TopStruct(# [: the carrier of X, the carrier of Y:],t #);

take T ; :: thesis: ( 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 ) } } )

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: verum

{ (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:]

proof

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:] ;
let e be object ; :: according to TARSKI:def 3 :: thesis: ( not 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 ) } } or e in bool [: the carrier of X, the carrier of Y:] )

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: e in bool [: the carrier of X, the carrier of Y:]

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: verum

end;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: e in bool [: the carrier of X, the carrier of Y:]

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: verum

set T = TopStruct(# [: the carrier of X, the carrier of Y:],t #);

now :: thesis: ( 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 #) & ( 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 #) ) & ( for a, b being Subset of TopStruct(# [: the carrier of X, the carrier of Y:],t #) st a in the topology of TopStruct(# [: the carrier of X, the carrier of Y:],t #) & b in the topology of TopStruct(# [: the carrier of X, the carrier of Y:],t #) holds

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

then reconsider T = TopStruct(# [: the carrier of X, the carrier of Y:],t #) as strict TopSpace by PRE_TOPC:def 1;union a in the topology of TopStruct(# [: the carrier of X, the carrier of Y:],t #) ) & ( for a, b being Subset of TopStruct(# [: the carrier of X, the carrier of Y:],t #) st a in the topology of TopStruct(# [: the carrier of X, the carrier of Y:],t #) & b in the topology of TopStruct(# [: the carrier of X, the carrier of Y:],t #) holds

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

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 ) }

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: ( ( 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 #) ) & ( for a, b being Subset of TopStruct(# [: the carrier of X, the carrier of Y:],t #) st a in the topology of TopStruct(# [: the carrier of X, the carrier of Y:],t #) & b in the topology of TopStruct(# [: the carrier of X, the carrier of Y:],t #) holds

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

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: for a, b being Subset of TopStruct(# [: the carrier of X, the carrier of Y:],t #) st a in the topology of TopStruct(# [: the carrier of X, the carrier of Y:],t #) & b in the topology of TopStruct(# [: the carrier of X, the carrier of Y:],t #) holds

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

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:]

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: a /\ b in the topology of TopStruct(# [: the carrier of X, the carrier of Y:],t #)

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

end;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

the carrier of TopStruct(# [: the carrier of X, the carrier of Y:],t #) = union A
;
let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in A or 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 ) } )

assume e in A ; :: thesis: 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 ) }

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: verum

end;assume e in A ; :: thesis: 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 ) }

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: verum

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: ( ( 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 #) ) & ( for a, b being Subset of TopStruct(# [: the carrier of X, the carrier of Y:],t #) st a in the topology of TopStruct(# [: the carrier of X, the carrier of Y:],t #) & b in the topology of TopStruct(# [: the carrier of X, the carrier of Y:],t #) holds

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

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: for a, b being Subset of TopStruct(# [: the carrier of X, the carrier of Y:],t #) st a in the topology of TopStruct(# [: the carrier of X, the carrier of Y:],t #) & b in the topology of TopStruct(# [: the carrier of X, the carrier of Y:],t #) holds

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

proof

let a, b be Subset of TopStruct(# [: the carrier of X, the carrier of Y:],t #); :: thesis: ( a in the topology of TopStruct(# [: the carrier of X, the carrier of Y:],t #) & b in the topology of TopStruct(# [: the carrier of X, the carrier of Y:],t #) implies a /\ b in the topology of TopStruct(# [: the carrier of X, the carrier of Y:],t #) )
let a be Subset-Family of TopStruct(# [: the carrier of X, the carrier of Y:],t #); :: thesis: ( a c= the topology of TopStruct(# [: the carrier of X, the carrier of Y:],t #) implies union a in the topology of TopStruct(# [: the carrier of X, the carrier of Y:],t #) )

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:]

( 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: union a in the topology of TopStruct(# [: the carrier of X, the carrier of Y:],t #)

A4: union A = union a

end;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

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
let e be object ; :: according to TARSKI:def 3 :: thesis: ( not 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 ) ) } or e in bool [: the carrier of X, the carrier of Y:] )

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: e in bool [: the carrier of X, the carrier of Y:]

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: verum

end;( x in a & [:X1,Y1:] c= x ) ) } or e in bool [: the carrier of X, the carrier of Y:] )

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: e in bool [: the carrier of X, the carrier of Y:]

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: verum

( 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: union a in the topology of TopStruct(# [: the carrier of X, the carrier of Y:],t #)

A4: union A = union a

proof

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 ) }
thus
union A c= union a
:: according to XBOOLE_0:def 10 :: thesis: union a c= union A

assume e in union a ; :: thesis: e in union A

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: verum

end;proof

let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in union a or e in union A )
let e1, e2 be object ; :: according to RELAT_1:def 3 :: thesis: ( not [e1,e2] in union A or [e1,e2] in union a )

assume [e1,e2] in union A ; :: thesis: [e1,e2] in union a

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: verum

end;assume [e1,e2] in union A ; :: thesis: [e1,e2] in union a

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: verum

assume e in union a ; :: thesis: e in union A

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: verum

proof

hence
union a in the topology of TopStruct(# [: the carrier of X, the carrier of Y:],t #)
by A4; :: thesis: verum
let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in A or 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 ) } )

assume e in A ; :: thesis: 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 ) }

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: verum

end;assume e in A ; :: thesis: 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 ) }

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: verum

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

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:] ;
let e be object ; :: according to TARSKI:def 3 :: thesis: ( not 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 ) } or e in bool [: the carrier of X, the carrier of Y:] )

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: e in bool [: the carrier of X, the carrier of Y:]

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: verum

end;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: e in bool [: the carrier of X, the carrier of Y:]

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: verum

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: a /\ b in the topology of TopStruct(# [: the carrier of X, the carrier of Y:],t #)

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

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 ) }
thus
a /\ b c= union C
:: according to XBOOLE_0:def 10 :: thesis: union C c= a /\ b

assume [e1,e2] in union C ; :: thesis: [e1,e2] in a /\ b

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: verum

end;proof

let e1, e2 be object ; :: according to RELAT_1:def 3 :: thesis: ( not [e1,e2] in union C or [e1,e2] in a /\ b )
let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in a /\ b or e in union C )

assume A22: e in a /\ b ; :: thesis: e in union C

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: verum

end;assume A22: e in a /\ b ; :: thesis: e in union C

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: verum

assume [e1,e2] in union C ; :: thesis: [e1,e2] in a /\ b

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: verum

proof

hence
a /\ b in the topology of TopStruct(# [: the carrier of X, the carrier of Y:],t #)
by A21; :: thesis: verum
let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in C or 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 ) } )

assume e in C ; :: thesis: 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 ) }

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: verum

end;assume e in C ; :: thesis: 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 ) }

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: verum

take T ; :: thesis: ( 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 ) } } )

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: verum