theorem Th28: :: DILWORTH:28

for R being RelStr
for S being Subset of R
for C being Clique of (subrelstr S) holds C is Clique of R