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
consider z being Element of Class EqR;
z is Subset of X by A2, TARSKI:def 3;
then ex x being set st
( x in X & z = Class EqR,x ) by A2, Def5;
hence contradiction by A1; :: thesis: verum