let n be Element of NAT ; :: thesis: 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); :: thesis: 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)) ` ; :: thesis: verum