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)
for X being Subset of S holds (TransEU f,g) . X = (SIGMA g) \/ ((SIGMA f) /\ (Pred X,R))
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)
for X being Subset of S holds (TransEU f,g) . X = (SIGMA g) \/ ((SIGMA f) /\ (Pred X,R))
let BASSIGN be non empty Subset of (ModelSP S); :: thesis: for f, g being Assign of (CTLModel R,BASSIGN)
for X being Subset of S holds (TransEU f,g) . X = (SIGMA g) \/ ((SIGMA f) /\ (Pred X,R))
let f, g be Assign of (CTLModel R,BASSIGN); :: thesis: for X being Subset of S holds (TransEU f,g) . X = (SIGMA g) \/ ((SIGMA f) /\ (Pred X,R))
let X be Subset of S; :: thesis: (TransEU f,g) . X = (SIGMA g) \/ ((SIGMA f) /\ (Pred X,R))
set h = Tau X,R,BASSIGN;
(TransEU f,g) . X = SigFoaxTau g,f,X,R,BASSIGN by Def73
.= (SIGMA g) \/ (SIGMA (Fax f,(Tau X,R,BASSIGN))) by Th33
.= (SIGMA g) \/ ((SIGMA f) /\ (SIGMA (EX (Tau X,R,BASSIGN)))) by Th33
.= (SIGMA g) \/ ((SIGMA f) /\ (Pred (SIGMA (Tau X,R,BASSIGN)),R)) by Th50 ;
hence (TransEU f,g) . X = (SIGMA g) \/ ((SIGMA f) /\ (Pred X,R)) by Th32; :: thesis: verum