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 (BASSModel (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 (BASSModel (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 (BASSModel (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 (BASSModel (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: ( 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 A3: 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 ex t being Element of S st
( s = t & t |= Foax (g,f,h) ) by A3;
hence s |= Foax (g,f,h) ; :: thesis: verum

end;

assume s |= Foax (g,f,h) ; :: thesis: s |= h
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: verum

end;

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

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

proof

assume A4: 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)
A5: for s being object st s in SIGMA (Foax (g,f,h)) holds
s in SIGMA h

proof

let x be object ; :: thesis: ( x in SIGMA (Foax (g,f,h)) implies x in SIGMA h )
assume x in SIGMA (Foax (g,f,h)) ; :: thesis: x in SIGMA h
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: verum

end;

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

proof

let x be object ; :: thesis: ( x in SIGMA h implies x in SIGMA (Foax (g,f,h)) )
assume x in SIGMA h ; :: thesis: x in SIGMA (Foax (g,f,h))
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: verum

end;

then SIGMA h = SIGMA (Foax (g,f,h)) by A5, TARSKI:2;
hence SIGMA h is_a_fixpoint_of TransEU (f,g) by A1, ABIAN:def 4; :: 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