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

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