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