ex S being Element of CQC-Sub-WFF st
( S `1 = p & S `2 = Sub ) by Th12;
hence [p,Sub] is Element of CQC-Sub-WFF by SUBSTUT1:10; :: thesis: verum