let X be set ; :: thesis: for EqR1, EqR2 being Equivalence_Relation of X holds
( not EqR1 \/ EqR2 = nabla X or EqR1 = nabla X or EqR2 = nabla X )
let EqR1, EqR2 be Equivalence_Relation of X; :: thesis: ( not EqR1 \/ EqR2 = nabla X or EqR1 = nabla X or EqR2 = nabla X )
assume A1: EqR1 \/ EqR2 = nabla X ; :: thesis: ( EqR1 = nabla X or EqR2 = nabla X )
( X = {} or EqR1 = nabla X or EqR2 = nabla X )

proof

consider y being Element of X;

A2: now

let x be set ; :: thesis: ( not x in X or Class EqR1,x = X or Class EqR2,x = X )
assume A3: x in X ; :: thesis: ( Class EqR1,x = X or Class EqR2,x = X )
then ( Class (nabla X),x = Class EqR1,x or Class (nabla X),x = Class EqR2,x ) by A1, Th37;
hence ( Class EqR1,x = X or Class EqR2,x = X ) by A3, Th34; :: thesis: verum

end;

assume X <> {} ; :: thesis: ( EqR1 = nabla X or EqR2 = nabla X )
then ( Class EqR1,y = X or Class EqR2,y = X ) by A2;
hence ( EqR1 = nabla X or EqR2 = nabla X ) by Th35; :: thesis: verum

end;

hence ( EqR1 = nabla X or EqR2 = nabla X ) ; :: thesis: verum