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 Th38
.= (((X `) (+) (B !)) `) (+) B by Th1
.= (((X (-) B) `) `) (+) B by Th38 ;
hence ((X `) (o) (B !)) ` = X (O) B ; :: thesis: verum