let i1, i2 be Integer; :: thesis: ( i1 * i2 = - 1 iff ( ( i1 = - 1 & i2 = 1 ) or ( i1 = 1 & i2 = - 1 ) ) )
thus ( not i1 * i2 = - 1 or ( i1 = - 1 & i2 = 1 ) or ( i1 = 1 & i2 = - 1 ) ) :: thesis: ( ( ( i1 = - 1 & i2 = 1 ) or ( i1 = 1 & i2 = - 1 ) ) implies i1 * i2 = - 1 )

proof

assume i1 * i2 = - 1 ; :: thesis: ( ( i1 = - 1 & i2 = 1 ) or ( i1 = 1 & i2 = - 1 ) )
then (- i1) * i2 = 1 ;
then ( ( - (- i1) = - 1 & i2 = 1 ) or ( - i1 = - 1 & i2 = - 1 ) ) by Th9;
hence ( ( i1 = - 1 & i2 = 1 ) or ( i1 = 1 & i2 = - 1 ) ) ; :: thesis: verum

end;

assume ( ( i1 = - 1 & i2 = 1 ) or ( i1 = 1 & i2 = - 1 ) ) ; :: thesis: i1 * i2 = - 1
hence i1 * i2 = - 1 ; :: thesis: verum