let X be non empty set ; :: thesis: for I being Ideal of X holds {} in I
let I be Ideal of X; :: thesis: {} in I
consider Y being Element of I;
( {} c= Y & {} c= X ) by XBOOLE_1:2;
hence {} in I by Def2; :: thesis: verum