theorem :: MODELC_1:23

for H 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 |= EG H iff ex pai being inf_path of R st
( pai . 0 = s & ( for n being Element of NAT holds pai . n,kai |= H ) ) )