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 :: thesis: for X, Y being set st X in A & Y in A holds
( X \/ Y in A & X \ Y in A )

let X, Y be set ; :: thesis: ( X in A & Y in A implies ( X \/ Y in A & X \ Y in A ) )
assume that
A2: X in A and
A3: Y in A ; :: thesis: ( X \/ Y in A & X \ Y in A )
reconsider Z = Y \ X as Element of A by A1, A2, A3;
X \/ Y = X \+\ Z by XBOOLE_1:98;
hence X \/ Y in A by A1, A2; :: thesis: X \ Y in A
thus X \ Y in A by A1, A2, A3; :: thesis: verum

end;

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