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