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

proof

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;

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