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 )
then reconsider Z1 = X \+\ Y, Z2 = X /\ Y as Element of A by A1;
X \/ Y = Z1 \+\ Z2 by XBOOLE_1:94;
hence X \/ Y in A by A1; :: thesis: X \ Y in A
X \ Y = X \+\ Z2 by XBOOLE_1:100;
hence X \ Y in A by A1, A2; :: thesis: verum

end;

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