let T be non empty right_complementable Abelian add-associative right_zeroed RLSStruct ; :: thesis: for X, B, Y being Subset of T holds X (O) B c= (X \/ Y) (O) B
let X, B, Y be Subset of T; :: 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