let S, T be non empty TopSpace; :: thesis: for G being Subset of st ( for x being Point of st x in G holds
ex GS being Subset of ex GT being Subset of st
( GS is open & GT is open & x in [:GS,GT:] & [:GS,GT:] c= G ) ) holds
G is open
let G be Subset of ; :: thesis: ( ( for x being Point of st x in G holds
ex GS being Subset of ex GT being Subset of 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 st x in G holds
ex GS being Subset of ex GT being Subset of 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 , GT is Subset of : ( GS is open & GT is open & [:GS,GT:] c= G ) } ;
{ [:GS,GT:] where GS is Subset of , GT is Subset of : ( 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 , GT is Subset of : ( 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 , GT is Subset of : ( GS is open & GT is open & [:GS,GT:] c= G ) } ; :: thesis: e in bool the carrier of [:S,T:]
then ex GS being Subset of ex GT being Subset of st
( e = [:GS,GT:] & GS is open & GT is open & [:GS,GT:] c= G ) ;
hence e in bool the carrier of [:S,T:] ; :: thesis: verum

end;

then reconsider A = { [:GS,GT:] where GS is Subset of , GT is Subset of : ( GS is open & GT is open & [:GS,GT:] c= G ) } as Subset-Family of ;
reconsider A = A as Subset-Family of ;
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 , GT being Subset of such that
A2: GS is open and
A3: GT is open and
A4: x in [:GS,GT:] and
A5: [: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 A2, A3, A4, A5; :: thesis: verum

end;

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

end;

then A8: G = union A by TARSKI:def 4;
for e being set st e in A holds
ex X1 being Subset of ex Y1 being Subset of 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 ex Y1 being Subset of st
( e = [:X1,Y1:] & X1 is open & Y1 is open ) )
assume e in A ; :: thesis: ex X1 being Subset of ex Y1 being Subset of st
( e = [:X1,Y1:] & X1 is open & Y1 is open )
then ex GS being Subset of ex GT being Subset of st
( e = [:GS,GT:] & GS is open & GT is open & [:GS,GT:] c= G ) ;
hence ex X1 being Subset of ex Y1 being Subset of st
( e = [:X1,Y1:] & X1 is open & Y1 is open ) ; :: thesis: verum

end;

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