let n be Element of NAT ; for X, B1, B2 being Subset of (TOP-REAL n) holds X (@) (B2,B1) = ((X `) (&) (B1,B2)) `
let X, B1, B2 be Subset of (TOP-REAL n); X (@) (B2,B1) = ((X `) (&) (B1,B2)) `
((X `) (&) (B1,B2)) ` =
((X \ (((X `) (-) B1) /\ (((X `) `) (-) B2))) `) `
by SUBSET_1:14
.=
X \ (X (*) (B2,B1))
;
hence
X (@) (B2,B1) = ((X `) (&) (B1,B2)) `
; verum