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
A1: s in {s} by TARSKI:def 1;
ex p being set st
( p in S & [s,p] in R ) by Lm30;
hence not R .: {s} is empty by A1, RELAT_1:def 13; :: thesis: verum