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
set Y = the Element of I;
( {} c= the Element of I & {} c= X ) ;
hence {} in I by Def2; :: thesis: verum