let X, Y be TopSpace; :: thesis: for B being Subset of [:X,Y:] holds

( B is open iff ex A being Subset-Family of [:X,Y:] st

( B = union A & ( for e being set st e in A holds

ex X1 being Subset of X ex Y1 being Subset of Y st

( e = [:X1,Y1:] & X1 is open & Y1 is open ) ) ) )

let B be Subset of [:X,Y:]; :: thesis: ( B is open iff ex A being Subset-Family of [:X,Y:] st

( B = union A & ( for e being set st e in A holds

ex X1 being Subset of X ex Y1 being Subset of Y st

( e = [:X1,Y1:] & X1 is open & Y1 is open ) ) ) )

A1: the topology of [:X,Y:] = { (union A) where A is Subset-Family of [:X,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 ) } } by Def2;

thus ( B is open implies ex A being Subset-Family of [:X,Y:] st

( B = union A & ( for e being set st e in A holds

ex X1 being Subset of X ex Y1 being Subset of Y st

( e = [:X1,Y1:] & X1 is open & Y1 is open ) ) ) ) :: thesis: ( ex A being Subset-Family of [:X,Y:] st

( B = union A & ( for e being set st e in A holds

ex X1 being Subset of X ex Y1 being Subset of Y st

( e = [:X1,Y1:] & X1 is open & Y1 is open ) ) ) implies B is open )

A6: for e being set st e in A holds

ex X1 being Subset of X ex Y1 being Subset of Y st

( e = [:X1,Y1:] & X1 is open & Y1 is open ) ; :: thesis: B is open

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

( B is open iff ex A being Subset-Family of [:X,Y:] st

( B = union A & ( for e being set st e in A holds

ex X1 being Subset of X ex Y1 being Subset of Y st

( e = [:X1,Y1:] & X1 is open & Y1 is open ) ) ) )

let B be Subset of [:X,Y:]; :: thesis: ( B is open iff ex A being Subset-Family of [:X,Y:] st

( B = union A & ( for e being set st e in A holds

ex X1 being Subset of X ex Y1 being Subset of Y st

( e = [:X1,Y1:] & X1 is open & Y1 is open ) ) ) )

A1: the topology of [:X,Y:] = { (union A) where A is Subset-Family of [:X,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 ) } } by Def2;

thus ( B is open implies ex A being Subset-Family of [:X,Y:] st

( B = union A & ( for e being set st e in A holds

ex X1 being Subset of X ex Y1 being Subset of Y st

( e = [:X1,Y1:] & X1 is open & Y1 is open ) ) ) ) :: thesis: ( ex A being Subset-Family of [:X,Y:] st

( B = union A & ( for e being set st e in A holds

ex X1 being Subset of X ex Y1 being Subset of Y st

( e = [:X1,Y1:] & X1 is open & Y1 is open ) ) ) implies B is open )

proof

given A being Subset-Family of [:X,Y:] such that A5:
B = union A
and
assume
B in the topology of [:X,Y:]
; :: according to PRE_TOPC:def 2 :: thesis: ex A being Subset-Family of [:X,Y:] st

( B = union A & ( for e being set st e in A holds

ex X1 being Subset of X ex Y1 being Subset of Y st

( e = [:X1,Y1:] & X1 is open & Y1 is open ) ) )

then consider A being Subset-Family of [:X,Y:] such that

A2: B = union A and

A3: 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 A1;

take A ; :: thesis: ( B = union A & ( for e being set st e in A holds

ex X1 being Subset of X ex Y1 being Subset of Y st

( e = [:X1,Y1:] & X1 is open & Y1 is open ) ) )

thus B = union A by A2; :: thesis: for e being set st e in A holds

ex X1 being Subset of X ex Y1 being Subset of Y st

( e = [:X1,Y1:] & X1 is open & Y1 is open )

let e be set ; :: thesis: ( e in A implies ex X1 being Subset of X ex Y1 being Subset of Y st

( e = [:X1,Y1:] & X1 is open & Y1 is open ) )

assume e in A ; :: thesis: ex X1 being Subset of X ex Y1 being Subset of Y st

( e = [:X1,Y1:] & X1 is open & Y1 is open )

then 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 A3;

then consider X1 being Subset of X, Y1 being Subset of Y such that

A4: ( e = [:X1,Y1:] & X1 in the topology of X & Y1 in the topology of Y ) ;

reconsider Y1 = Y1 as Subset of Y ;

reconsider X1 = X1 as Subset of X ;

take X1 ; :: thesis: ex Y1 being Subset of Y st

( e = [:X1,Y1:] & X1 is open & Y1 is open )

take Y1 ; :: thesis: ( e = [:X1,Y1:] & X1 is open & Y1 is open )

thus ( e = [:X1,Y1:] & X1 is open & Y1 is open ) by A4; :: thesis: verum

end;( B = union A & ( for e being set st e in A holds

ex X1 being Subset of X ex Y1 being Subset of Y st

( e = [:X1,Y1:] & X1 is open & Y1 is open ) ) )

then consider A being Subset-Family of [:X,Y:] such that

A2: B = union A and

A3: 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 A1;

take A ; :: thesis: ( B = union A & ( for e being set st e in A holds

ex X1 being Subset of X ex Y1 being Subset of Y st

( e = [:X1,Y1:] & X1 is open & Y1 is open ) ) )

thus B = union A by A2; :: thesis: for e being set st e in A holds

ex X1 being Subset of X ex Y1 being Subset of Y st

( e = [:X1,Y1:] & X1 is open & Y1 is open )

let e be set ; :: thesis: ( e in A implies ex X1 being Subset of X ex Y1 being Subset of Y st

( e = [:X1,Y1:] & X1 is open & Y1 is open ) )

assume e in A ; :: thesis: ex X1 being Subset of X ex Y1 being Subset of Y st

( e = [:X1,Y1:] & X1 is open & Y1 is open )

then 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 A3;

then consider X1 being Subset of X, Y1 being Subset of Y such that

A4: ( e = [:X1,Y1:] & X1 in the topology of X & Y1 in the topology of Y ) ;

reconsider Y1 = Y1 as Subset of Y ;

reconsider X1 = X1 as Subset of X ;

take X1 ; :: thesis: ex Y1 being Subset of Y st

( e = [:X1,Y1:] & X1 is open & Y1 is open )

take Y1 ; :: thesis: ( e = [:X1,Y1:] & X1 is open & Y1 is open )

thus ( e = [:X1,Y1:] & X1 is open & Y1 is open ) by A4; :: thesis: verum

A6: for e being set st e in A holds

ex X1 being Subset of X ex Y1 being Subset of Y st

( e = [:X1,Y1:] & X1 is open & Y1 is open ) ; :: thesis: B is open

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

hence
B in the topology of [:X,Y:]
by A1, A5; :: according to PRE_TOPC:def 2 :: thesis: verum
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 consider X1 being Subset of X, Y1 being Subset of Y such that

A7: e = [:X1,Y1:] and

A8: ( X1 is open & Y1 is open ) by A6;

( X1 in the topology of X & Y1 in the topology of Y ) by A8;

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 A7; :: 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 consider X1 being Subset of X, Y1 being Subset of Y such that

A7: e = [:X1,Y1:] and

A8: ( X1 is open & Y1 is open ) by A6;

( X1 in the topology of X & Y1 in the topology of Y ) by A8;

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 A7; :: thesis: verum