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 \ (X \ Y) by XBOOLE_1:48;
hence X /\ Y is Element of A ; :: thesis: verum