let X be set ; :: thesis: ( not X is empty & X is preBoolean implies X is with_empty_element )
assume A1: ( not X is empty & X is preBoolean ) ; :: thesis: X is with_empty_element
then consider x being object such that
A2: x in X ;
reconsider x1 = x as set by A2;
{} = x1 \ x1 by XBOOLE_1:37;
then {} in X by A1, A2, FINSUB_1:def 3;
hence X is with_empty_element ; :: thesis: verum