let X be set ; :: thesis: for EqR being Equivalence_Relation of X st X = {} holds
Class EqR = {}
let EqR be Equivalence_Relation of X; :: thesis: ( X = {} implies Class EqR = {} )
assume that
A1: X = {} and
A2: Class EqR <> {} ; :: thesis: contradiction
set z = the Element of Class EqR;
the Element of Class EqR is Subset of X by A2, TARSKI:def 3;
then ex x being object st
( x in X & the Element of Class EqR = Class (EqR,x) ) by A2, Def3;
hence contradiction by A1; :: thesis: verum