let Q be multLoop; :: thesis: [#] (lp (Nucl Q)) = Nucl Q
A1: 1. Q in Nucl Q by Th20;
A2: for x, y being Element of Q st x in Nucl Q & y in Nucl Q holds
x * y in Nucl Q by Th21;
A3: for x, y being Element of Q st x in Nucl Q & y in Nucl Q holds
x \ y in Nucl Q by Th22;
for x, y being Element of Q st x in Nucl Q & y in Nucl Q holds
x / y in Nucl Q by Th23;
hence [#] (lp (Nucl Q)) = Nucl Q by Th18, A1, A2, A3; :: thesis: verum