:: deftheorem Def50 defines And_0 MODELC_1:def 50 :
for S being non empty set
for f, g being set
for b₄ being Element of ModelSP S holds
( b₄ = And_0 (f,g,S) iff for s being set st s in S holds
( (Castboolean ((Fid (f,S)) . s)) '&' (Castboolean ((Fid (g,S)) . s)) = TRUE iff (Fid (b₄,S)) . s = TRUE ) );