let X be set ; :: thesis: for EqR1, EqR2, E being Equivalence_Relation of X st E = EqR1 \/ EqR2 holds

for x being object 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 object 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 object holds

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

for x being object holds

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

( not x in X or Class (E,x) = Class (EqR1,x) or Class (E,x) = Class (EqR2,x) ) ; :: thesis: verum

for x being object 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 object 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 object holds

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

for x being object holds

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

proof

hence
for x being object holds
let x be object ; :: 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 object 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;

consider z being object 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;

not [z,x] in EqR2 by A9, A10, Th19;

then A14: [z,x] in EqR1 by A1, A13, XBOOLE_0:def 3;

then A17: [y,x] in EqR2 by A1, A8, XBOOLE_0:def 3;

then [y,z] in E by A8, Th7;

hence contradiction by A1, A18, A15, XBOOLE_0:def 3; :: thesis: verum

end;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 object 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 :: thesis: ( y in Class (EqR1,x) implies y in Class (E,x) )

then A8:
[y,x] in E
by A4, Th19;assume that

A6: y in Class (EqR1,x) and

A7: not y in Class (E,x) ; :: thesis: contradiction

[y,x] in EqR1 by A6, Th19;

then [y,x] in E by A1, XBOOLE_0:def 3;

hence contradiction by A7, Th19; :: thesis: verum

end;A6: y in Class (EqR1,x) and

A7: not y in Class (E,x) ; :: thesis: contradiction

[y,x] in EqR1 by A6, Th19;

then [y,x] in E by A1, XBOOLE_0:def 3;

hence contradiction by A7, Th19; :: thesis: verum

consider z being object 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 :: thesis: ( z in Class (EqR2,x) implies z in Class (E,x) )

then A13:
[z,x] in E
by A9, Th19;assume that

A11: z in Class (EqR2,x) and

A12: not z in Class (E,x) ; :: thesis: contradiction

[z,x] in EqR2 by A11, Th19;

then [z,x] in E by A1, XBOOLE_0:def 3;

hence contradiction by A12, Th19; :: thesis: verum

end;A11: z in Class (EqR2,x) and

A12: not z in Class (E,x) ; :: thesis: contradiction

[z,x] in EqR2 by A11, Th19;

then [z,x] in E by A1, XBOOLE_0:def 3;

hence contradiction by A12, Th19; :: thesis: verum

not [z,x] in EqR2 by A9, A10, Th19;

then A14: [z,x] in EqR1 by A1, A13, XBOOLE_0:def 3;

A15: now :: thesis: not [y,z] in EqR1

not [y,x] in EqR1
by A4, A5, Th19;assume
[y,z] in EqR1
; :: thesis: contradiction

then A16: [z,y] in EqR1 by Th6;

[x,z] in EqR1 by A14, Th6;

then [x,y] in EqR1 by A16, Th7;

then [y,x] in EqR1 by Th6;

hence contradiction by A4, A5, Th19; :: thesis: verum

end;then A16: [z,y] in EqR1 by Th6;

[x,z] in EqR1 by A14, Th6;

then [x,y] in EqR1 by A16, Th7;

then [y,x] in EqR1 by Th6;

hence contradiction by A4, A5, Th19; :: thesis: verum

then A17: [y,x] in EqR2 by A1, A8, XBOOLE_0:def 3;

A18: now :: thesis: not [y,z] in EqR2

[x,z] in E
by A13, Th6;assume A19:
[y,z] in EqR2
; :: thesis: contradiction

[x,y] in EqR2 by A17, Th6;

then [x,z] in EqR2 by A19, Th7;

then [z,x] in EqR2 by Th6;

hence contradiction by A9, A10, Th19; :: thesis: verum

end;[x,y] in EqR2 by A17, Th6;

then [x,z] in EqR2 by A19, Th7;

then [z,x] in EqR2 by Th6;

hence contradiction by A9, A10, Th19; :: thesis: verum

then [y,z] in E by A8, Th7;

hence contradiction by A1, A18, A15, XBOOLE_0:def 3; :: thesis: verum

( not x in X or Class (E,x) = Class (EqR1,x) or Class (E,x) = Class (EqR2,x) ) ; :: thesis: verum