let x, y be R_eal; :: thesis: ( x * y = 0. iff ( x = 0. or y = 0. ) )
( not x * y = 0. or x = 0. or y = 0. )

proof

assume A1: x * y = 0. ; :: thesis: ( x = 0. or y = 0. )
assume A2: ( x <> 0. & y <> 0. ) ; :: thesis: contradiction

now

per cases ( ( x < 0. & y < 0. ) or ( 0. < x & 0. < y ) or ( x < 0. & 0. < y ) or ( 0. < x & y < 0. ) ) by A2;

suppose ( ( x < 0. & y < 0. ) or ( 0. < x & 0. < y ) ) ; :: thesis: contradiction

hence contradiction by A1, Th20; :: thesis: verum

end;

suppose ( ( x < 0. & 0. < y ) or ( 0. < x & y < 0. ) ) ; :: thesis: contradiction

hence contradiction by A1, Th21; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

hence ( x * y = 0. iff ( x = 0. or y = 0. ) ) by Def1; :: thesis: verum