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 (EG f) = gfp S,(TransEG f)
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 (EG f) = gfp S,(TransEG f)
let BASSIGN be non empty Subset of (ModelSP S); :: thesis: for f being Assign of (CTLModel R,BASSIGN) holds SIGMA (EG f) = gfp S,(TransEG f)
let f be Assign of (CTLModel R,BASSIGN); :: thesis: SIGMA (EG f) = gfp S,(TransEG f)
set g = EG f;
set h = Tau (gfp S,(TransEG f)),R,BASSIGN;
A1: SIGMA (Tau (gfp S,(TransEG f)),R,BASSIGN) = gfp S,(TransEG f) by Th32;
then SIGMA (Tau (gfp S,(TransEG f)),R,BASSIGN) is_a_fixpoint_of TransEG f by KNASTER:7;
then A2: for s being Element of S holds
( s |= Tau (gfp S,(TransEG f)),R,BASSIGN iff s |= Fax f,(Tau (gfp S,(TransEG f)),R,BASSIGN) ) by Th42;
A3: SIGMA (Tau (gfp S,(TransEG f)),R,BASSIGN) c= SIGMA (EG f)

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in SIGMA (Tau (gfp S,(TransEG f)),R,BASSIGN) or x in SIGMA (EG f) )
assume x in SIGMA (Tau (gfp S,(TransEG f)),R,BASSIGN) ; :: thesis: x in SIGMA (EG f)
then consider s being Element of S such that
A4: x = s and
A5: s |= Tau (gfp S,(TransEG f)),R,BASSIGN ;
s |= EG f by A2, A5, Th41;
hence x in SIGMA (EG f) by A4; :: thesis: verum

end;

for s being Element of S holds
( s |= EG f iff s |= Fax f,(EG f) ) by Th39;
then SIGMA (EG f) is_a_fixpoint_of TransEG f by Th42;
then SIGMA (EG f) c= gfp S,(TransEG f) by KNASTER:10;
hence SIGMA (EG f) = gfp S,(TransEG f) by A1, A3, XBOOLE_0:def 10; :: thesis: verum