for G being non empty symmetric irreflexive RelStr
for a, b, c, d being Element of G
for Z being Subset of G st Z = {a,b,c,d} & a,b,c,d are_mutually_distinct & [a,b] in the InternalRel of G & [b,c] in the InternalRel of G & [c,d] in the InternalRel of G & not [a,c] in the InternalRel of G & not [a,d] in the InternalRel of G & not [b,d] in the InternalRel of G holds
subrelstr Z embeds Necklace 4