:: deftheorem defines |= MODELC_2:def 57 :
for S being non empty set
for BASSIGN being non empty Subset of (ModelSP (Inf_seq S))
for t being Element of Inf_seq S
for f being Assign of (Inf_seqModel (S,BASSIGN)) holds
( t |= f iff (Fid (f,(Inf_seq S))) . t = TRUE );