take {} L ; :: thesis: for x, y being set st x in {} L & y in {} L & not [x,y] in R & not x = y holds
[y,x] in R
thus for x, y being set st x in {} L & y in {} L & not [x,y] in R & not x = y holds
[y,x] in R ; :: thesis: verum