let X be non empty set ; for R being Relation of X
for x, y being Element of X st not [x,y] in R ` holds
[x,y] in R
let R be Relation of X; for x, y being Element of X st not [x,y] in R ` holds
[x,y] in R
let x, y be Element of X; ( not [x,y] in R ` implies [x,y] in R )
assume A2:
not [x,y] in R `
; [x,y] in R
R \/ (R `) = [#] [:X,X:]
by SUBSET_1:10;
hence
[x,y] in R
by A2, XBOOLE_0:def 3; verum