let H be CTL-formula; :: thesis:
let S be non empty set ; :: thesis:
let R be total Relation of S,S; :: thesis:
let s be Element of S; :: thesis:
let BASSIGN be non empty Subset of (ModelSP S); :: thesis:
let kai be Function of atomic_WFF ,the BasicAssign of (BASSModel R,BASSIGN); :: thesis:
A1: ( ex pai being inf_path of R st
( pai . 0 = s & ( for n being Element of NAT holds pai . n |= Evaluate H,kai ) ) implies ex pai being inf_path of R st
( pai . 0 = s & ( for n being Element of NAT holds pai . n,kai |= H ) ) )

given pai being inf_path of R such that A2: pai . 0 = s and
A3: for n being Element of NAT holds pai . n |= Evaluate H,kai ; :: thesis:
take pai ; :: thesis:
for n being Element of NAT holds pai . n,kai |= H

let n be Element of NAT ; :: thesis:
pai . n |= Evaluate H,kai by A3;
hence pai . n,kai |= H by Def60; :: thesis:

end;

hence ( pai . 0 = s & ( for n being Element of NAT holds pai . n,kai |= H ) ) by A2; :: thesis:

end;

A4: ( ex pai being inf_path of R st
( pai . 0 = s & ( for n being Element of NAT holds pai . n,kai |= H ) ) implies ex pai being inf_path of R st
( pai . 0 = s & ( for n being Element of NAT holds pai . n |= Evaluate H,kai ) ) )

given pai being inf_path of R such that A5: pai . 0 = s and
A6: for n being Element of NAT holds pai . n,kai |= H ; :: thesis:
take pai ; :: thesis:
for n being Element of NAT holds pai . n |= Evaluate H,kai

let n be Element of NAT ; :: thesis:
pai . n,kai |= H by A6;
hence pai . n |= Evaluate H,kai by Def60; :: thesis:

end;

hence ( pai . 0 = s & ( for n being Element of NAT holds pai . n |= Evaluate H,kai ) ) by A5; :: thesis:

end;