|:S:| = EmptyMS I by Def3;
hence |:S:| is empty-yielding ; :: thesis: verum