theorem Th22: :: MYCIELSK:22

for R being RelStr
for C being StableSet of (ComplRelStr R) holds C is Clique of R