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, h being Assign of (CTLModel R,BASSIGN) holds
( ( for s being Element of S holds
( s |= h iff s |= Foax g,f,h ) ) iff SIGMA h is_a_fixpoint_of TransEU f,g )
let R be total Relation of S,S; :: thesis: for BASSIGN being non empty Subset of (ModelSP S)
for f, g, h being Assign of (CTLModel R,BASSIGN) holds
( ( for s being Element of S holds
( s |= h iff s |= Foax g,f,h ) ) iff SIGMA h is_a_fixpoint_of TransEU f,g )
let BASSIGN be non empty Subset of (ModelSP S); :: thesis: for f, g, h being Assign of (CTLModel R,BASSIGN) holds
( ( for s being Element of S holds
( s |= h iff s |= Foax g,f,h ) ) iff SIGMA h is_a_fixpoint_of TransEU f,g )
let f, g, h be Assign of (CTLModel R,BASSIGN); :: thesis: ( ( for s being Element of S holds
( s |= h iff s |= Foax g,f,h ) ) iff SIGMA h is_a_fixpoint_of TransEU f,g )
set H = SIGMA h;
set Q = SIGMA (Foax g,f,h);
A1: (TransEU f,g) . (SIGMA h) = SigFoaxTau g,f,(SIGMA h),R,BASSIGN by Def73
.= SIGMA (Foax g,f,h) by Th31 ;
A2: ( ( for s being Element of S holds
( s |= h iff s |= Foax g,f,h ) ) implies SIGMA h is_a_fixpoint_of TransEU f,g )

proof

assume A3: for s being Element of S holds
( s |= h iff s |= Foax g,f,h ) ; :: thesis: SIGMA h is_a_fixpoint_of TransEU f,g
A4: for x being set st x in SIGMA h holds
x in SIGMA (Foax g,f,h)

proof

let x be set ; :: thesis: ( x in SIGMA h implies x in SIGMA (Foax g,f,h) )
assume A5: x in SIGMA h ; :: thesis: x in SIGMA (Foax g,f,h)
consider s being Element of S such that
A6: x = s and
A7: s |= h by A5;
s |= Foax g,f,h by A3, A7;
hence x in SIGMA (Foax g,f,h) by A6; :: thesis: verum

end;

for s being set st s in SIGMA (Foax g,f,h) holds
s in SIGMA h

proof

let x be set ; :: thesis: ( x in SIGMA (Foax g,f,h) implies x in SIGMA h )
assume A8: x in SIGMA (Foax g,f,h) ; :: thesis: x in SIGMA h
consider s being Element of S such that
A9: x = s and
A10: s |= Foax g,f,h by A8;
s |= h by A3, A10;
hence x in SIGMA h by A9; :: thesis: verum

end;

then SIGMA h = SIGMA (Foax g,f,h) by A4, TARSKI:2;
hence SIGMA h is_a_fixpoint_of TransEU f,g by A1, ABIAN:def 4; :: thesis: verum

end;

( SIGMA h is_a_fixpoint_of TransEU f,g implies for s being Element of S holds
( s |= h iff s |= Foax g,f,h ) )

proof

assume SIGMA h is_a_fixpoint_of TransEU f,g ; :: thesis: for s being Element of S holds
( s |= h iff s |= Foax g,f,h )
then A11: SIGMA h = SIGMA (Foax g,f,h) by A1, ABIAN:def 4;
for s being Element of S holds
( s |= h iff s |= Foax g,f,h )

proof

let s be Element of S; :: thesis: ( s |= h iff s |= Foax g,f,h )
thus ( s |= h implies s |= Foax g,f,h ) :: thesis: ( s |= Foax g,f,h implies s |= h )

proof

assume s |= h ; :: thesis: s |= Foax g,f,h
then s in SIGMA h ;
then consider t being Element of S such that
A12: s = t and
A13: t |= Foax g,f,h by A11;
thus s |= Foax g,f,h by A12, A13; :: thesis: verum

end;

assume s |= Foax g,f,h ; :: thesis: s |= h
then s in SIGMA (Foax g,f,h) ;
then consider t being Element of S such that
A14: s = t and
A15: t |= h by A11;
thus s |= h by A14, A15; :: thesis: verum

end;

hence for s being Element of S holds
( s |= h iff s |= Foax g,f,h ) ; :: thesis: verum

end;

hence ( ( for s being Element of S holds
( s |= h iff s |= Foax g,f,h ) ) iff SIGMA h is_a_fixpoint_of TransEU f,g ) by A2; :: thesis: verum