let n be Element of NAT ; :: thesis: for X, B, Y being Subset of (TOP-REAL n) holds X (O) B c= (X \/ Y) (O) B
let X, B, Y be Subset of (TOP-REAL n); :: thesis: X (O) B c= (X \/ Y) (O) B
X c= X \/ Y by XBOOLE_1:7;
hence X (O) B c= (X \/ Y) (O) B by Th45; :: thesis: verum