let a, b, c be Nat; :: thesis: ((a + b) - c) mod 3 = (((a mod 3) + (b mod 3)) + (2 * (c mod 3))) mod 3
thus ((a + b) - c) mod 3 = (((a + b) - c) + (c * 3)) mod 3 by EULER_1:12
.= (a + (b + (2 * c))) mod 3
.= ((a mod 3) + ((b + (2 * c)) mod 3)) mod 3 by NAT_D:66
.= (((a mod 3) mod 3) + (((b mod 3) + ((c + c) mod 3)) mod 3)) mod 3 by NAT_D:66
.= (((a mod 3) mod 3) + (((b mod 3) + (((c mod 3) + (c mod 3)) mod 3)) mod 3)) mod 3 by NAT_D:66
.= (((a mod 3) mod 3) + (((b mod 3) + ((c mod 3) + (c mod 3))) mod 3)) mod 3 by Th88
.= ((a mod 3) + ((b mod 3) + ((c mod 3) + (c mod 3)))) mod 3 by Th88
.= (((a mod 3) + (b mod 3)) + (2 * (c mod 3))) mod 3 ; :: thesis: verum