:: deftheorem defines Lap ROUGHS_2:def 9 :
for R being non empty RelStr
for X being Subset of R holds Lap X = (UAp (X `)) ` ;