:: deftheorem Def6 defines implicative FILTER_0:def 6 :
for IT being non empty LattStr holds
( IT is implicative iff for p, q being Element of IT ex r being Element of IT st
( p "/\" r [= q & ( for r1 being Element of IT st p "/\" r1 [= q holds
r1 [= r ) ) );