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 )
proof
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;
given A being Subset-Family of [:X,Y:] such that A5: B = union A and
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
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;
hence B in the topology of [:X,Y:] by A1, A5; :: according to PRE_TOPC:def 2 :: thesis: verum