:: deftheorem MeetDef defines MeetTBA LATTBA_1:def 9 :
for T being Ternary_Boolean_Algebra
for x being Element of T
for b₃ being BinOp of the carrier of T holds
( b₃ = MeetTBA (T,x) iff for a, b being Element of T holds b₃ . (a,b) = Tern (a,(x `),b) );