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