let S be non empty set ; :: thesis: for R being total Relation of S,S
for BASSIGN being non empty Subset of (ModelSP S)
for f, g being Assign of (CTLModel R,BASSIGN) st ( for s being Element of S holds
( s |= g iff s |= Fax f,g ) ) holds
for s being Element of S st s |= g holds
s |= EG f
let R be total Relation of S,S; :: thesis: for BASSIGN being non empty Subset of (ModelSP S)
for f, g being Assign of (CTLModel R,BASSIGN) st ( for s being Element of S holds
( s |= g iff s |= Fax f,g ) ) holds
for s being Element of S st s |= g holds
s |= EG f
let BASSIGN be non empty Subset of (ModelSP S); :: thesis: for f, g being Assign of (CTLModel R,BASSIGN) st ( for s being Element of S holds
( s |= g iff s |= Fax f,g ) ) holds
for s being Element of S st s |= g holds
s |= EG f
let f, g be Assign of (CTLModel R,BASSIGN); :: thesis: ( ( for s being Element of S holds
( s |= g iff s |= Fax f,g ) ) implies for s being Element of S st s |= g holds
s |= EG f )
assume A1: for s being Element of S holds
( s |= g iff s |= Fax f,g ) ; :: thesis: for s being Element of S st s |= g holds
s |= EG f
A2: for s being Element of S st s |= g holds
s |= EX g

proof

let s be Element of S; :: thesis: ( s |= g implies s |= EX g )
assume s |= g ; :: thesis: s |= EX g
then s |= f '&' (EX g) by A1;
hence s |= EX g by Th13; :: thesis: verum

end;

for s0 being Element of S st s0 |= g holds
s0 |= EG f

proof

let s0 be Element of S; :: thesis: ( s0 |= g implies s0 |= EG f )
assume s0 |= g ; :: thesis: s0 |= EG f
then consider pai being inf_path of R such that
A3: pai . 0 = s0 and
A4: for n being Element of NAT holds pai . n |= g by A2, Th40;
for n being Element of NAT holds pai . n |= f

proof

let n be Element of NAT ; :: thesis: pai . n |= f
pai . n |= g by A4;
then pai . n |= f '&' (EX g) by A1;
hence pai . n |= f by Th13; :: thesis: verum

end;

hence s0 |= EG f by A3, Th15; :: thesis: verum

end;

hence for s being Element of S st s |= g holds
s |= EG f ; :: thesis: verum