:: deftheorem defines satisfying(7H') ROUGHS_3:def 11 :
for R being non empty RelStr holds
( R is satisfying(7H') iff for X being Subset of R holds (UAp X) ` c= UAp ((UAp X) `) );