set B = { [:X1,Y1:] where X1 is Subset of X, Y1 is Subset of Y : ( [:X1,Y1:] c= A & X1 is open & Y1 is open ) } ;

{ [:X1,Y1:] where X1 is Subset of X, Y1 is Subset of Y : ( [:X1,Y1:] c= A & X1 is open & Y1 is open ) } c= bool the carrier of [:X,Y:]

{ [:X1,Y1:] where X1 is Subset of X, Y1 is Subset of Y : ( [:X1,Y1:] c= A & X1 is open & Y1 is open ) } c= bool the carrier of [:X,Y:]

proof

hence
{ [:X1,Y1:] where X1 is Subset of X, Y1 is Subset of Y : ( [:X1,Y1:] c= A & X1 is open & Y1 is open ) } is Subset-Family of [:X,Y:]
; :: thesis: verum
let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in { [:X1,Y1:] where X1 is Subset of X, Y1 is Subset of Y : ( [:X1,Y1:] c= A & X1 is open & Y1 is open ) } or e in bool the carrier of [:X,Y:] )

assume e in { [:X1,Y1:] where X1 is Subset of X, Y1 is Subset of Y : ( [:X1,Y1:] c= A & X1 is open & Y1 is open ) } ; :: thesis: e in bool the carrier of [:X,Y:]

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

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

hence e in bool the carrier of [:X,Y:] ; :: thesis: verum

end;assume e in { [:X1,Y1:] where X1 is Subset of X, Y1 is Subset of Y : ( [:X1,Y1:] c= A & X1 is open & Y1 is open ) } ; :: thesis: e in bool the carrier of [:X,Y:]

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

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

hence e in bool the carrier of [:X,Y:] ; :: thesis: verum