let x be even Integer; :: thesis: for y, z being odd Integer holds
( not (x * y) * z = 8 or ( x = 8 & y = 1 & z = 1 ) or ( x = 8 & y = - 1 & z = - 1 ) or ( x = - 8 & y = 1 & z = - 1 ) or ( x = - 8 & y = - 1 & z = 1 ) )
let y, z be odd Integer; :: thesis: ( not (x * y) * z = 8 or ( x = 8 & y = 1 & z = 1 ) or ( x = 8 & y = - 1 & z = - 1 ) or ( x = - 8 & y = 1 & z = - 1 ) or ( x = - 8 & y = - 1 & z = 1 ) )
assume (x * y) * z = 8 ; :: thesis: ( ( x = 8 & y = 1 & z = 1 ) or ( x = 8 & y = - 1 & z = - 1 ) or ( x = - 8 & y = 1 & z = - 1 ) or ( x = - 8 & y = - 1 & z = 1 ) )
then ( ( x * y = 8 & z = 1 ) or ( x * y = - 8 & z = - 1 ) ) by Lm3, Lm10;
hence ( ( x = 8 & y = 1 & z = 1 ) or ( x = 8 & y = - 1 & z = - 1 ) or ( x = - 8 & y = 1 & z = - 1 ) or ( x = - 8 & y = - 1 & z = 1 ) ) by Lm3, Lm4, Lm10; :: thesis: verum