let A be non empty preBoolean set ; :: thesis: {} in A
consider x being Element of A;
x \ x = {} by XBOOLE_1:37;
hence {} in A ; :: thesis: verum