let n be Element of NAT ; :: thesis: for X, B being Subset of (TOP-REAL n) holds ((X `) (O) (B !)) ` = X (o) B
let X, B be Subset of (TOP-REAL n); :: thesis: ((X `) (O) (B !)) ` = X (o) B
((X `) (O) (B !)) ` = (((((X `) (-) (B !)) `) (-) B) `) ` by Th37
.= (X (+) ((B !) !)) (-) B by Th37
.= (X (+) B) (-) B by Th1 ;
hence ((X `) (O) (B !)) ` = X (o) B ; :: thesis: verum