for X being set
for L being List of X
for O being Operation of X holds L WHERE O c= L by Th3;