:: deftheorem Def49 defines And_0 MODELC_2:def 49 :
for S being non empty set
for f, g being set
for b₄ being Element of ModelSP (Inf_seq S) holds
( b₄ = And_0 (f,g,S) iff for t being set st t in Inf_seq S holds
( (Castboolean ((Fid (f,(Inf_seq S))) . t)) '&' (Castboolean ((Fid (g,(Inf_seq S))) . t)) = TRUE iff (Fid (b₄,(Inf_seq S))) . t = TRUE ) );