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) )
proof
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;
A5: now :: thesis: ( y in Class (EqR1,x) implies y in Class (E,x) )
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;
then A8: [y,x] in E by A4, Th19;
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) )
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;
then A13: [z,x] in E by A9, Th19;
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
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;
not [y,x] in EqR1 by A4, A5, Th19;
then A17: [y,x] in EqR2 by A1, A8, XBOOLE_0:def 3;
A18: now :: thesis: not [y,z] in EqR2
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,z] in E by A13, Th6;
then [y,z] in E by A8, Th7;
hence contradiction by A1, A18, A15, XBOOLE_0:def 3; :: thesis: verum
end;
hence for x being object holds
( not x in X or Class (E,x) = Class (EqR1,x) or Class (E,x) = Class (EqR2,x) ) ; :: thesis: verum