Sub | X = (@ Sub) | X ;
hence Sub | X is CQC_Substitution by PARTFUN1:119; :: thesis: verum