let Q be multLoop; :: thesis: ( 1. Q in [#] (lp (Cent Q)) & 1. Q in Cent Q )
the OneF of (lp (Cent Q)) = 1. Q by Def30;
then 1. Q in [#] (lp (Cent Q)) ;
hence ( 1. Q in [#] (lp (Cent Q)) & 1. Q in Cent Q ) by Th25; :: thesis: verum