let S be non empty set ; :: thesis: for R being total Relation of S,S
for s being Element of S holds not R .: {s} is empty
let R be total Relation of S,S; :: thesis: for s being Element of S holds not R .: {s} is empty
let s be Element of S; :: thesis: not R .: {s} is empty
consider p being set such that
p in S and
A1: [s,p] in R by Lm31;
s in {s} by TARSKI:def 1;
hence not R .: {s} is empty by A1, RELAT_1:def 13; :: thesis: verum