let x, y, z be even Integer; :: thesis: ( not (x * y) * z = 8 or ( x = 2 & y = 2 & z = 2 ) or ( x = - 2 & y = - 2 & z = 2 ) or ( x = - 2 & y = 2 & z = - 2 ) or ( x = 2 & y = - 2 & z = - 2 ) )
assume (x * y) * z = 8 ; :: thesis: ( ( x = 2 & y = 2 & z = 2 ) or ( x = - 2 & y = - 2 & z = 2 ) or ( x = - 2 & y = 2 & z = - 2 ) or ( x = 2 & y = - 2 & z = - 2 ) )
then ( ( x * y = 2 & z = 4 ) or ( x * y = 4 & z = 2 ) or ( x * y = - 2 & z = - 4 ) or ( x * y = - 4 & z = - 2 ) ) by Lm3, Lm9;
hence ( ( x = 2 & y = 2 & z = 2 ) or ( x = - 2 & y = - 2 & z = 2 ) or ( x = - 2 & y = 2 & z = - 2 ) or ( x = 2 & y = - 2 & z = - 2 ) ) by Lm6, Lm9, Lm5, Lm7, Lm8; :: thesis: verum