theorem :: MODELC_1:24

for H1, H2 being CTL-formula
for S being non empty set
for R being total Relation of S,S
for s being Element of S
for BASSIGN being non empty Subset of (ModelSP S)
for kai being Function of atomic_WFF, the BasicAssign of (BASSModel (R,BASSIGN)) holds
( s,kai |= H1 EU H2 iff ex pai being inf_path of R st
( pai . 0 = s & ex m being Element of NAT st
( ( for j being Element of NAT st j < m holds
pai . j,kai |= H1 ) & pai . m,kai |= H2 ) ) )