Michael Kohlhase Armin Fiedler 1999-08-30 , if or . or We prove the assertion by a case analysis over . If , then . . by definition of . , then . . , by definition of . We have considered both cases from , so we have or .