for L being non empty RelStr
for S being non empty full SubRelStr of L
for X being set holds S |^ X is full SubRelStr of L |^ X