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

now

let X, Y be set ; :: thesis: ( X in A & Y in A implies ( X \/ Y in A & X \ Y in A ) )
assume A2: ( X in A & Y in A ) ; :: thesis: ( X \/ Y in A & X \ Y in A )
hence X \/ Y in A by A1; :: thesis: X \ Y in A
reconsider Z1 = X \+\ Y, Z2 = X \/ Y as Element of A by A1, A2;
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: verum

end;

hence A is preBoolean by Th10; :: thesis: verum