theorem Th1: :: AOFA_A00:1

for A, B being set
for R being b₁ -valued Relation holds R .: B c= A