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