:: deftheorem Def51 defines And_ MODELC_1:def 51 :
for S being non empty set
for b₂ being BinOp of (ModelSP S) holds
( b₂ = And_ S iff for f, g being set st f in ModelSP S & g in ModelSP S holds
b₂ . (f,g) = And_0 (f,g,S) );