let S be non empty set ; :: thesis: for R being total Relation of S,S
for s being Element of S
for BASSIGN being non empty Subset of (ModelSP S)
for f being Assign of (CTLModel R,BASSIGN) holds
( s |= EX f iff ex pai being inf_path of R st
( pai . 0 = s & pai . 1 |= f ) )
let R be total Relation of S,S; :: thesis: for s being Element of S
for BASSIGN being non empty Subset of (ModelSP S)
for f being Assign of (CTLModel R,BASSIGN) holds
( s |= EX f iff ex pai being inf_path of R st
( pai . 0 = s & pai . 1 |= f ) )
let s be Element of S; :: thesis: for BASSIGN being non empty Subset of (ModelSP S)
for f being Assign of (CTLModel R,BASSIGN) holds
( s |= EX f iff ex pai being inf_path of R st
( pai . 0 = s & pai . 1 |= f ) )
let BASSIGN be non empty Subset of (ModelSP S); :: thesis: for f being Assign of (CTLModel R,BASSIGN) holds
( s |= EX f iff ex pai being inf_path of R st
( pai . 0 = s & pai . 1 |= f ) )
let f be Assign of (CTLModel R,BASSIGN); :: thesis: ( s |= EX f iff ex pai being inf_path of R st
( pai . 0 = s & pai . 1 |= f ) )
A1: EX f = EneXt_0 f,R by Def46;
A2: ( s |= EX f implies ex pai being inf_path of R st
( pai . 0 = s & pai . 1 |= f ) )

proof

assume s |= EX f ; :: thesis: ex pai being inf_path of R st
( pai . 0 = s & pai . 1 |= f )
then (Fid (EneXt_0 f,R),S) . s = TRUE by A1, Def59;
then EneXt_univ s,(Fid f,S),R = TRUE by Def45;
then consider pai being inf_path of R such that
A3: pai . 0 = s and
A4: (Fid f,S) . (pai . 1) = TRUE by Def44;
take pai ; :: thesis: ( pai . 0 = s & pai . 1 |= f )
thus ( pai . 0 = s & pai . 1 |= f ) by A3, A4, Def59; :: thesis: verum

end;

( ex pai being inf_path of R st
( pai . 0 = s & pai . 1 |= f ) implies s |= EX f )

proof

assume A5: ex pai being inf_path of R st
( pai . 0 = s & pai . 1 |= f ) ; :: thesis: s |= EX f
ex pai being inf_path of R st
( pai . 0 = s & (Fid f,S) . (pai . 1) = TRUE )

proof

consider pai being inf_path of R such that
A6: pai . 0 = s and
A7: pai . 1 |= f by A5;
take pai ; :: thesis: ( pai . 0 = s & (Fid f,S) . (pai . 1) = TRUE )
thus ( pai . 0 = s & (Fid f,S) . (pai . 1) = TRUE ) by A6, A7, Def59; :: thesis: verum

end;

then EneXt_univ s,(Fid f,S),R = TRUE by Def44;
then (Fid (EX f),S) . s = TRUE by A1, Def45;
hence s |= EX f by Def59; :: thesis: verum

end;

hence ( s |= EX f iff ex pai being inf_path of R st
( pai . 0 = s & pai . 1 |= f ) ) by A2; :: thesis: verum