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:2;

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:2;

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