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 )
( not X <> {} or EqR1 = nabla X or EqR2 = nabla X )

proof

set y = the Element of X;

A2: now :: thesis: for x being object holds
( not x in X or Class (EqR1,x) = X or Class (EqR2,x) = X )

let x be object ; :: 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, Th29;
hence ( Class (EqR1,x) = X or Class (EqR2,x) = X ) by A3, Th26; :: thesis: verum

end;

assume X <> {} ; :: thesis: ( EqR1 = nabla X or EqR2 = nabla X )
then ( Class (EqR1, the Element of X) = X or Class (EqR2, the Element of X) = X ) by A2;
hence ( EqR1 = nabla X or EqR2 = nabla X ) by Th27; :: thesis: verum

end;

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