:: deftheorem Def17 defines LCongruence OSAFREE:def 17 :
for S being locally_directed OrderSortedSign
for X being non-empty ManySortedSet of S
for b₃ being monotone OSCongruence of ParsedTermsOSA X holds
( b₃ = LCongruence X iff for R being monotone OSCongruence of ParsedTermsOSA X holds b₃ c= R );