theorem Th58: :: MODELC_2:58

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, g being Assign of (Inf_seqModel (S,BASSIGN)) holds
( t |= f '&' g iff ( t |= f & t |= g ) )