let S be non empty set ; :: thesis:
let R be total Relation of S,S; :: thesis:
let BASSIGN be non empty Subset of (ModelSP S); :: thesis:
let f, g, h be Assign of (CTLModel R,BASSIGN); :: thesis:
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: ( 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 ) )

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

assume s |= h ; :: thesis:
then s in SIGMA h ;
then ex t being Element of S st
( s = t & t |= Foax g,f,h ) by A3;
hence s |= Foax g,f,h ; :: thesis:

end;

assume s |= Foax g,f,h ; :: thesis:
then s in SIGMA (Foax g,f,h) ;
then ex t being Element of S st
( s = t & t |= h ) by A3;
hence s |= h ; :: thesis:

end;

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

end;

( ( 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 )

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

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

end;

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

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

end;

end;