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