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;

consider z being set such that
A8: ( ( 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;

A9: now

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

end;

A12: [y,x] in E by A4, A5, Th27;
not [y,x] in EqR1 by A4, A5, Th27;
then A13: [y,x] in EqR2 by A1, A12, XBOOLE_0:def 3;
A14: [z,x] in E by A8, A9, Th27;
then [x,z] in E by Th12;
then A15: [y,z] in E by A12, Th13;
not [z,x] in EqR2 by A8, A9, Th27;
then A16: [z,x] in EqR1 by A1, A14, XBOOLE_0:def 3;

A17: now

assume A18: [y,z] in EqR2 ; :: thesis: contradiction
[x,y] in EqR2 by A13, Th12;
then [x,z] in EqR2 by A18, Th13;
then [z,x] in EqR2 by Th12;
hence contradiction by A8, A9, Th27; :: thesis: verum

end;

now

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

end;

hence contradiction by A1, A15, A17, 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