theorem Th1: :: VALUED_0:1

for R being Relation
for S being complex-valued Relation st R c= S holds
R is complex-valued