for A being QC-alphabet
for S1, S2, S19, S29 being Element of QC-Sub-WFF A st S1 `2 = S2 `2 & S19 `2 = S29 `2 & Sub_& (S1,S2) = Sub_& (S19,S29) holds
( S1 = S19 & S2 = S29 )