theorem :: MATHMORP:73

for n being Element of NAT
for X, B1, B2 being Subset of (TOP-REAL n) holds X (@) (B2,B1) = ((X `) (&) (B1,B2)) `