let A be non empty set ; :: thesis:
assume A1: for X, Y being Element of A holds
( X \+\ Y in A & X \/ Y in A ) ; :: thesis:

let X, Y be set ; :: thesis:
assume that
A2: X in A and
A3: Y in A ; :: thesis:
thus X \/ Y in A by A1, A2, A3; :: thesis:
reconsider Z1 = X \+\ Y, Z2 = X \/ Y as Element of A by A1, A2, A3;
X /\ Y = Z1 \+\ Z2 by XBOOLE_1:95;
then reconsider Z = X /\ Y as Element of A by A1;
X \ Y = X \+\ Z by XBOOLE_1:100;
hence X \ Y in A by A1, A2; :: thesis:

end;