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 f = { s where s is Element of S : (Fid f,S) . s = TRUE }
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 f = { s where s is Element of S : (Fid f,S) . s = TRUE }
let BASSIGN be non empty Subset of (ModelSP S); :: thesis: for f being Assign of (CTLModel R,BASSIGN) holds SIGMA f = { s where s is Element of S : (Fid f,S) . s = TRUE }
let f be Assign of (CTLModel R,BASSIGN); :: thesis: SIGMA f = { s where s is Element of S : (Fid f,S) . s = TRUE }
A1: for x being set st x in SIGMA f holds
x in { s where s is Element of S : (Fid f,S) . s = TRUE }

proof

let x be set ; :: thesis: ( x in SIGMA f implies x in { s where s is Element of S : (Fid f,S) . s = TRUE } )
assume x in SIGMA f ; :: thesis: x in { s where s is Element of S : (Fid f,S) . s = TRUE }
then consider s being Element of S such that
A2: x = s and
A3: s |= f ;
(Fid f,S) . s = TRUE by A3, Def59;
hence x in { s where s is Element of S : (Fid f,S) . s = TRUE } by A2; :: thesis: verum

end;

for x being set st x in { s where s is Element of S : (Fid f,S) . s = TRUE } holds
x in SIGMA f

proof

let x be set ; :: thesis: ( x in { s where s is Element of S : (Fid f,S) . s = TRUE } implies x in SIGMA f )
assume x in { s where s is Element of S : (Fid f,S) . s = TRUE } ; :: thesis: x in SIGMA f
then consider s being Element of S such that
A4: x = s and
A5: (Fid f,S) . s = TRUE ;
s |= f by A5, Def59;
hence x in SIGMA f by A4; :: thesis: verum

end;

hence SIGMA f = { s where s is Element of S : (Fid f,S) . s = TRUE } by A1, TARSKI:2; :: thesis: verum