:: deftheorem defines Pred MODELC_1:def 62 :
for S being non empty set
for R being total Relation of S,S
for H being Subset of S holds Pred (H,R) = { s where s is Element of S : ex t being Element of S st
( t in H & [s,t] in R ) } ;