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