let R be Relation; :: thesis: ( ( for x, y being set holds not [x,y] in R ) implies R = {} )
assume A1: for x, y being set holds not [x,y] in R ; :: thesis: R = {}
assume A2: not R = {} ; :: thesis: contradiction
then ex x, y being set st the Element of R = [x,y] by Def1;
hence contradiction by A1, A2; :: thesis: verum