( Trivial-multLoopStr is satisfying_TT & Trivial-multLoopStr is satisfying_TL & Trivial-multLoopStr is satisfying_TR & Trivial-multLoopStr is satisfying_LR & Trivial-multLoopStr is satisfying_LL & Trivial-multLoopStr is satisfying_RR & Trivial-multLoopStr is satisfying_aa1 & Trivial-multLoopStr is satisfying_aa2 & Trivial-multLoopStr is satisfying_aa3 & Trivial-multLoopStr is satisfying_Ka & Trivial-multLoopStr is satisfying_aK1 & Trivial-multLoopStr is satisfying_aK2 & Trivial-multLoopStr is satisfying_aK3 ) by ALGSTR_1:9;
hence ex b₁ being multLoop st
( b₁ is strict & b₁ is satisfying_TT & b₁ is satisfying_TL & b₁ is satisfying_TR & b₁ is satisfying_LR & b₁ is satisfying_LL & b₁ is satisfying_RR & b₁ is satisfying_aa1 & b₁ is satisfying_aa2 & b₁ is satisfying_aa3 & b₁ is satisfying_Ka & b₁ is satisfying_aK1 & b₁ is satisfying_aK2 & b₁ is satisfying_aK3 ) ; :: thesis: verum