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