theorem Th1: :: FRIENDS1:1

for R being Relation holds card R = card (R ~)