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 (CTLModel R,BASSIGN); :: thesis:
A1: ( ex pai being inf_path of R st
( pai . 0 = s & pai . 1 |= Evaluate H,kai ) implies ex pai being inf_path of R st
( pai . 0 = s & pai . 1,kai |= H ) )

given pai being inf_path of R such that A2: pai . 0 = s and
A3: pai . 1 |= Evaluate H,kai ; :: thesis:
take pai ; :: thesis:
thus ( pai . 0 = s & pai . 1,kai |= H ) by A2, A3, Def60; :: thesis:

end;

A4: ( ex pai being inf_path of R st
( pai . 0 = s & pai . 1,kai |= H ) implies ex pai being inf_path of R st
( pai . 0 = s & pai . 1 |= Evaluate H,kai ) )

given pai being inf_path of R such that A5: pai . 0 = s and
A6: pai . 1,kai |= H ; :: thesis:
take pai ; :: thesis:
thus ( pai . 0 = s & pai . 1 |= Evaluate H,kai ) by A5, A6, Def60; :: thesis:

end;