theorem Th29: :: DILWORTH:29

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