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 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
A2: x = s and
A3: s |= EX f ;
consider s1 being Element of S such that
A4: [s,s1] in R and
A5: s1 |= f by A3, Th28;
s1 in SIGMA f by A5;
hence x in Pred (SIGMA f),R by A2, A4; :: thesis: verum

end;

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
A6: x = s and
A7: ex s1 being Element of S st
( s1 in SIGMA f & [s,s1] in R ) ;
consider s1 being Element of S such that
A8: s1 in SIGMA f and
A9: [s,s1] in R by A7;
consider s2 being Element of S such that
A10: s1 = s2 and
A11: s2 |= f by A8;
s |= EX f by A9, A10, A11, Th28;
hence x in SIGMA (EX f) by A6; :: thesis: verum

end;

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