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

reconsider A = A as Subset-Family of [:S,T:] ;

for x being object holds

( x in G iff ex Y being set st

( x in Y & Y in A ) )

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 )

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

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:] ;
let e be object ; :: 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 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 e in bool the carrier of [:S,T:] ; :: thesis: verum

end;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 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 e in bool the carrier of [:S,T:] ; :: thesis: verum

reconsider A = A as Subset-Family of [:S,T:] ;

for x being object holds

( x in G iff ex Y being set st

( x in Y & Y in A ) )

proof

then A8:
G = union A
by TARSKI:def 4;
let x be object ; :: 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 )

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

hence x in G by A6; :: thesis: verum

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

given Y being set such that A6:
x in Y
and
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

A2: GS is open and

A3: GT is open and

A4: x in [:GS,GT:] and

A5: [:GS,GT:] c= G by A1;

take [:GS,GT:] ; :: thesis: ( x in [:GS,GT:] & [:GS,GT:] in A )

thus ( x in [:GS,GT:] & [:GS,GT:] in A ) by A2, A3, A4, A5; :: thesis: verum

end;( x in Y & Y in A )

then consider GS being Subset of S, GT being Subset of T 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 [:GS,GT:] ; :: thesis: ( x in [:GS,GT:] & [:GS,GT:] in A )

thus ( x in [:GS,GT:] & [:GS,GT:] in A ) by A2, A3, A4, A5; :: thesis: verum

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

hence x in G by A6; :: thesis: verum

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

hence
G is open
by A8, BORSUK_1:5; :: thesis: verum
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;( 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