let Q be multLoop; :: thesis: 1. Q in Nucl Q
A1: 1. Q in Nucl_l Q by Th20a;
1. Q in Nucl_m Q by Th20b;
hence 1. Q in Nucl Q by A1, Th12, Th20c; :: thesis: verum