:: deftheorem defines Inf_seqModel MODELC_2:def 56 :
for S being non empty set
for BASSIGN being non empty Subset of (ModelSP (Inf_seq S)) holds Inf_seqModel (S,BASSIGN) = LTLModelStr(# (ModelSP (Inf_seq S)),BASSIGN,(And_ S),(Or_ S),(Not_ S),(Next_ S),(Until_ S),(Release_ S) #);