let S, T be non empty TopSpace; :: thesis: for G being Subset of [:S,T:] st ( for x being Point of [:S,T:] st x in G holds
ex GS being Subset of S ex GT being Subset of T st
( GS is open & GT is open & x in [:GS,GT:] & [:GS,GT:] c= G ) ) holds
G is open
let G be Subset of [:S,T:]; :: thesis: ( ( for x being Point of [:S,T:] st x in G holds
ex GS being Subset of S ex GT being Subset of T st
( GS is open & GT is open & x in [:GS,GT:] & [:GS,GT:] c= G ) ) implies G is open )
assume A1: for x being Point of [:S,T:] st x in G holds
ex GS being Subset of S ex GT being Subset of T st
( GS is open & GT is open & x in [:GS,GT:] & [:GS,GT:] c= G ) ; :: thesis: G is open
set A = { [:GS,GT:] where GS is Subset of S, GT is Subset of T : ( GS is open & GT is open & [:GS,GT:] c= G ) } ;
{ [:GS,GT:] where GS is Subset of S, GT is Subset of T : ( GS is open & GT is open & [:GS,GT:] c= G ) } c= bool the carrier of [:S,T:]

proof

let e be set ; :: according to TARSKI:def 3 :: thesis: ( not e in { [:GS,GT:] where GS is Subset of S, GT is Subset of T : ( GS is open & GT is open & [:GS,GT:] c= G ) } or e in bool the carrier of [:S,T:] )
assume e in { [:GS,GT:] where GS is Subset of S, GT is Subset of T : ( GS is open & GT is open & [:GS,GT:] c= G ) } ; :: thesis: e in bool the carrier of [:S,T:]
then consider GS being Subset of S, GT being Subset of T such that
A2: e = [:GS,GT:] and
( GS is open & GT is open & [:GS,GT:] c= G ) ;
thus e in bool the carrier of [:S,T:] by A2; :: thesis: verum

end;

then reconsider A = { [:GS,GT:] where GS is Subset of S, GT is Subset of T : ( GS is open & GT is open & [:GS,GT:] c= G ) } as Subset-Family of [:S,T:] ;
reconsider A = A as Subset-Family of [:S,T:] ;
for x being set holds
( x in G iff ex Y being set st
( x in Y & Y in A ) )

proof

let x be set ; :: thesis: ( x in G iff ex Y being set st
( x in Y & Y in A ) )
thus ( x in G implies ex Y being set st
( x in Y & Y in A ) ) :: thesis: ( ex Y being set st
( x in Y & Y in A ) implies x in G )

proof

assume x in G ; :: thesis: ex Y being set st
( x in Y & Y in A )
then consider GS being Subset of S, GT being Subset of T such that
A3: ( GS is open & GT is open & x in [:GS,GT:] & [:GS,GT:] c= G ) by A1;
take Y = [:GS,GT:]; :: thesis: ( x in Y & Y in A )
thus ( x in Y & Y in A ) by A3; :: thesis: verum

end;

given Y being set such that A4: x in Y and
A5: Y in A ; :: thesis: x in G
ex GS being Subset of S ex GT being Subset of T st
( Y = [:GS,GT:] & GS is open & GT is open & [:GS,GT:] c= G ) by A5;
hence x in G by A4; :: thesis: verum

end;

then A6: G = union A by TARSKI:def 4;
for e being set st e in A holds
ex X1 being Subset of S ex Y1 being Subset of T st
( e = [:X1,Y1:] & X1 is open & Y1 is open )

proof

let e be set ; :: thesis: ( e in A implies ex X1 being Subset of S ex Y1 being Subset of T st
( e = [:X1,Y1:] & X1 is open & Y1 is open ) )
assume e in A ; :: thesis: ex X1 being Subset of S ex Y1 being Subset of T st
( e = [:X1,Y1:] & X1 is open & Y1 is open )
then ex GS being Subset of S ex GT being Subset of T st
( e = [:GS,GT:] & GS is open & GT is open & [:GS,GT:] c= G ) ;
hence ex X1 being Subset of S ex Y1 being Subset of T st
( e = [:X1,Y1:] & X1 is open & Y1 is open ) ; :: thesis: verum

end;

hence G is open by A6, BORSUK_1:45; :: thesis: verum