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, g being Assign of (CTLModel R,BASSIGN) holds SIGMA (f EU g) = lfp S,(TransEU f,g)
let R be total Relation of S,S; :: thesis: for BASSIGN being non empty Subset of (ModelSP S)
for f, g being Assign of (CTLModel R,BASSIGN) holds SIGMA (f EU g) = lfp S,(TransEU f,g)
let BASSIGN be non empty Subset of (ModelSP S); :: thesis: for f, g being Assign of (CTLModel R,BASSIGN) holds SIGMA (f EU g) = lfp S,(TransEU f,g)
let f, g be Assign of (CTLModel R,BASSIGN); :: thesis: SIGMA (f EU g) = lfp S,(TransEU f,g)
set h = f EU g;
for s being Element of S holds
( s |= f EU g iff s |= Foax g,f,(f EU g) ) by Th46;
then SIGMA (f EU g) is_a_fixpoint_of TransEU f,g by Th48;
then A1: lfp S,(TransEU f,g) c= SIGMA (f EU g) by KNASTER:10;
set p = Tau (lfp S,(TransEU f,g)),R,BASSIGN;
A2: SIGMA (Tau (lfp S,(TransEU f,g)),R,BASSIGN) = lfp S,(TransEU f,g) by Th32;
lfp S,(TransEU f,g) is_a_fixpoint_of TransEU f,g by KNASTER:6;
then A3: for s being Element of S holds
( s |= Tau (lfp S,(TransEU f,g)),R,BASSIGN iff s |= Foax g,f,(Tau (lfp S,(TransEU f,g)),R,BASSIGN) ) by A2, Th48;
SIGMA (f EU g) c= SIGMA (Tau (lfp S,(TransEU f,g)),R,BASSIGN)

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in SIGMA (f EU g) or x in SIGMA (Tau (lfp S,(TransEU f,g)),R,BASSIGN) )
assume x in SIGMA (f EU g) ; :: thesis: x in SIGMA (Tau (lfp S,(TransEU f,g)),R,BASSIGN)
then consider s being Element of S such that
A4: x = s and
A5: s |= f EU g ;
s |= Tau (lfp S,(TransEU f,g)),R,BASSIGN by A3, A5, Th47;
hence x in SIGMA (Tau (lfp S,(TransEU f,g)),R,BASSIGN) by A4; :: thesis: verum

end;

hence SIGMA (f EU g) = lfp S,(TransEU f,g) by A1, A2, XBOOLE_0:def 10; :: thesis: verum