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