theorem Th33: :: NECKLA_3:33

for R being symmetric irreflexive RelStr st card the carrier of R = 2 & the carrier of R in FinSETS holds
RelStr(# the carrier of R, the InternalRel of R #) in fin_RelStr_sp