let X, Y be set ; :: thesis: for A being non empty preBoolean set st X is Element of A & Y is Element of A holds
X \+\ Y is Element of A
let A be non empty preBoolean set ; :: thesis: ( X is Element of A & Y is Element of A implies X \+\ Y is Element of A )
assume ( X is Element of A & Y is Element of A ) ; :: thesis: X \+\ Y is Element of A
then reconsider X = X, Y = Y as Element of A ;
X \+\ Y = (X \ Y) \/ (Y \ X) ;
hence X \+\ Y is Element of A ; :: thesis: verum