let X be set ; :: thesis: for EqR1, EqR2, E being Equivalence_Relation of X st E = EqR1 \/ EqR2 holds
for x being set holds
( not x in X or Class (E,x) = Class (EqR1,x) or Class (E,x) = Class (EqR2,x) )
let EqR1, EqR2, E be Equivalence_Relation of X; :: thesis: ( E = EqR1 \/ EqR2 implies for x being set holds
( not x in X or Class (E,x) = Class (EqR1,x) or Class (E,x) = Class (EqR2,x) ) )
assume A1: E = EqR1 \/ EqR2 ; :: thesis: for x being set holds
( not x in X or Class (E,x) = Class (EqR1,x) or Class (E,x) = Class (EqR2,x) )
for x being set holds
( not x in X or Class (E,x) = Class (EqR1,x) or Class (E,x) = Class (EqR2,x) )

proof

let x be set ; :: thesis: ( not x in X or Class (E,x) = Class (EqR1,x) or Class (E,x) = Class (EqR2,x) )
assume x in X ; :: thesis: ( Class (E,x) = Class (EqR1,x) or Class (E,x) = Class (EqR2,x) )
assume that
A2: not Class (E,x) = Class (EqR1,x) and
A3: not Class (E,x) = Class (EqR2,x) ; :: thesis: contradiction
consider y being set such that
A4: ( ( y in Class (E,x) & not y in Class (EqR1,x) ) or ( y in Class (EqR1,x) & not y in Class (E,x) ) ) by A2, TARSKI:1;

A5: now

assume that
A6: y in Class (EqR1,x) and
A7: not y in Class (E,x) ; :: thesis: contradiction
[y,x] in EqR1 by A6, Th27;
then [y,x] in E by A1, XBOOLE_0:def 3;
hence contradiction by A7, Th27; :: thesis: verum

end;

then A8: [y,x] in E by A4, Th27;
consider z being set such that
A9: ( ( z in Class (E,x) & not z in Class (EqR2,x) ) or ( z in Class (EqR2,x) & not z in Class (E,x) ) ) by A3, TARSKI:1;

A10: now

assume that
A11: z in Class (EqR2,x) and
A12: not z in Class (E,x) ; :: thesis: contradiction
[z,x] in EqR2 by A11, Th27;
then [z,x] in E by A1, XBOOLE_0:def 3;
hence contradiction by A12, Th27; :: thesis: verum

end;

then A13: [z,x] in E by A9, Th27;
not [z,x] in EqR2 by A9, A10, Th27;
then A14: [z,x] in EqR1 by A1, A13, XBOOLE_0:def 3;

A15: now

assume [y,z] in EqR1 ; :: thesis: contradiction
then A16: [z,y] in EqR1 by Th12;
[x,z] in EqR1 by A14, Th12;
then [x,y] in EqR1 by A16, Th13;
then [y,x] in EqR1 by Th12;
hence contradiction by A4, A5, Th27; :: thesis: verum

end;

not [y,x] in EqR1 by A4, A5, Th27;
then A17: [y,x] in EqR2 by A1, A8, XBOOLE_0:def 3;

A18: now

assume A19: [y,z] in EqR2 ; :: thesis: contradiction
[x,y] in EqR2 by A17, Th12;
then [x,z] in EqR2 by A19, Th13;
then [z,x] in EqR2 by Th12;
hence contradiction by A9, A10, Th27; :: thesis: verum

end;

[x,z] in E by A13, Th12;
then [y,z] in E by A8, Th13;
hence contradiction by A1, A18, A15, XBOOLE_0:def 3; :: thesis: verum

end;

hence for x being set holds
( not x in X or Class (E,x) = Class (EqR1,x) or Class (E,x) = Class (EqR2,x) ) ; :: thesis: verum