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

let x be object ; :: 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;

let x be object ; :: 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;