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 & 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, Def62; :: 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, Def62; :: thesis:

end;