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 being Assign of (CTLModel R,BASSIGN) holds SIGMA (EX f) = Pred (SIGMA f),R
let R be total Relation of S,S; :: thesis: for BASSIGN being non empty Subset of (ModelSP S)
for f being Assign of (CTLModel R,BASSIGN) holds SIGMA (EX f) = Pred (SIGMA f),R
let BASSIGN be non empty Subset of (ModelSP S); :: thesis: for f being Assign of (CTLModel R,BASSIGN) holds SIGMA (EX f) = Pred (SIGMA f),R
let f be Assign of (CTLModel R,BASSIGN); :: thesis: SIGMA (EX f) = Pred (SIGMA f),R
set g = EX f;
set H = SIGMA f;
A1: for x being set st x in Pred (SIGMA f),R holds
x in SIGMA (EX f)

proof

let x be set ; :: thesis: ( x in Pred (SIGMA f),R implies x in SIGMA (EX f) )
assume x in Pred (SIGMA f),R ; :: thesis: x in SIGMA (EX f)
then consider s being Element of S such that
A2: x = s and
A3: ex s1 being Element of S st
( s1 in SIGMA f & [s,s1] in R ) ;
consider s1 being Element of S such that
A4: s1 in SIGMA f and
A5: [s,s1] in R by A3;
ex s2 being Element of S st
( s1 = s2 & s2 |= f ) by A4;
then s |= EX f by A5, Th28;
hence x in SIGMA (EX f) by A2; :: thesis: verum

end;

for x being set st x in SIGMA (EX f) holds
x in Pred (SIGMA f),R

proof

let x be set ; :: thesis: ( x in SIGMA (EX f) implies x in Pred (SIGMA f),R )
assume x in SIGMA (EX f) ; :: thesis: x in Pred (SIGMA f),R
then consider s being Element of S such that
A6: x = s and
A7: s |= EX f ;
consider s1 being Element of S such that
A8: [s,s1] in R and
A9: s1 |= f by A7, Th28;
s1 in SIGMA f by A9;
hence x in Pred (SIGMA f),R by A6, A8; :: thesis: verum

end;

hence SIGMA (EX f) = Pred (SIGMA f),R by A1, TARSKI:2; :: thesis: verum