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 )

( 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

hence
( EqR1 = nabla X or EqR2 = nabla X )
; :: thesis: verum
set y = the Element of 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;A2: now :: thesis: for x being object holds

( not x in X or Class (EqR1,x) = X or Class (EqR2,x) = X )

assume
X <> {}
; :: thesis: ( EqR1 = nabla X or EqR2 = nabla X )( 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 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

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