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 (BASSModel (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 (BASSModel (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 (BASSModel (R,BASSIGN)) holds SIGMA (EG f) = gfp (S,(TransEG f))
let f be Assign of (BASSModel (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:5;
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 object ; :: 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:8;
hence SIGMA (EG f) = gfp (S,(TransEG f)) by A1, A3, XBOOLE_0:def 10; :: thesis: verum