Class (E,(0. X)) in Class E by EQREL_1:def 3;
hence not Class E is empty ; :: thesis: verum