consider S being Element of CQC-Sub-WFF such that
A1: ( S `1 = p & S `2 = Sub ) by Th12;
thus [p,Sub] is Element of CQC-Sub-WFF by A1, SUBSTUT1:10; :: thesis: verum