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