consider F being strict Field;
for x, y being Element of F ex z being Element of F st
( z divides x & z divides y & ( for zz being Element of F st zz divides x & zz divides y holds
zz divides z ) ) by Lm1;
then F is gcd-like by Def11;
hence ex b₁ being non empty multLoopStr_0 st
( b₁ is gcd-like & b₁ is associative & b₁ is commutative & b₁ is well-unital ) ; :: thesis: verum