let X be set ; 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; ( not EqR1 \/ EqR2 = nabla X or EqR1 = nabla X or EqR2 = nabla X )
assume A1:
EqR1 \/ EqR2 = nabla X
; ( 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 for x being object holds
( not x in X or Class (EqR1,x) = X or Class (EqR2,x) = X )let x be
object ;
( not x in X or Class (EqR1,x) = X or Class (EqR2,x) = X )assume A3:
x in X
;
( 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;
verum end;
assume
X <> {}
;
( 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;
verum
end;
hence
( EqR1 = nabla X or EqR2 = nabla X )
; verum