|:S:| = [0] I by Def4;
hence |:S:| is empty-yielding ; :: thesis: verum