let X be non empty set ; :: thesis: 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; :: thesis: 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; :: thesis: ( not [x,y] in R ` implies [x,y] in R )
assume A2: not [x,y] in R ` ; :: thesis: [x,y] in R
R \/ (R `) = [#] [:X,X:] by SUBSET_1:10;
hence [x,y] in R by A2, XBOOLE_0:def 3; :: thesis: verum