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, h1, h2 being Assign of (CTLModel R,BASSIGN) st ( for s being Element of S st s |= h1 holds
s |= h2 ) holds
for s being Element of S st s |= Foax g,f,h1 holds
s |= Foax g,f,h2
let R be total Relation of S,S; :: thesis: for BASSIGN being non empty Subset of (ModelSP S)
for f, g, h1, h2 being Assign of (CTLModel R,BASSIGN) st ( for s being Element of S st s |= h1 holds
s |= h2 ) holds
for s being Element of S st s |= Foax g,f,h1 holds
s |= Foax g,f,h2
let BASSIGN be non empty Subset of (ModelSP S); :: thesis: for f, g, h1, h2 being Assign of (CTLModel R,BASSIGN) st ( for s being Element of S st s |= h1 holds
s |= h2 ) holds
for s being Element of S st s |= Foax g,f,h1 holds
s |= Foax g,f,h2
let f, g, h1, h2 be Assign of (CTLModel R,BASSIGN); :: thesis: ( ( for s being Element of S st s |= h1 holds
s |= h2 ) implies for s being Element of S st s |= Foax g,f,h1 holds
s |= Foax g,f,h2 )
assume A1: for s being Element of S st s |= h1 holds
s |= h2 ; :: thesis: for s being Element of S st s |= Foax g,f,h1 holds
s |= Foax g,f,h2
let s be Element of S; :: thesis: ( s |= Foax g,f,h1 implies s |= Foax g,f,h2 )
assume A2: s |= Foax g,f,h1 ; :: thesis: s |= Foax g,f,h2

per cases ( s |= g or s |= Fax f,h1 ) by A2, Th17;

suppose s |= g ; :: thesis: s |= Foax g,f,h2

hence s |= Foax g,f,h2 by Th17; :: thesis: verum

end;

suppose A3: s |= Fax f,h1 ; :: thesis: s |= Foax g,f,h2

then s |= EX h1 by Th13;
then consider pai being inf_path of R such that
A4: pai . 0 = s and
A5: pai . 1 |= h1 by Th14;
pai . 1 |= h2 by A1, A5;
then A6: s |= EX h2 by A4, Th14;
s |= f by A3, Th13;
then s |= f '&' (EX h2) by A6, Th13;
hence s |= Foax g,f,h2 by Th17; :: thesis: verum

end;

end;