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 (BASSModel R,BASSIGN) holds
( ( for s being Element of S holds
( s |= g iff s |= Fax f,g ) ) iff SIGMA g is_a_fixpoint_of TransEG f )
let R be total Relation of S,S; :: thesis: for BASSIGN being non empty Subset of (ModelSP S)
for f, g being Assign of (BASSModel R,BASSIGN) holds
( ( for s being Element of S holds
( s |= g iff s |= Fax f,g ) ) iff SIGMA g is_a_fixpoint_of TransEG f )
let BASSIGN be non empty Subset of (ModelSP S); :: thesis: for f, g being Assign of (BASSModel R,BASSIGN) holds
( ( for s being Element of S holds
( s |= g iff s |= Fax f,g ) ) iff SIGMA g is_a_fixpoint_of TransEG f )
let f, g be Assign of (BASSModel R,BASSIGN); :: thesis: ( ( for s being Element of S holds
( s |= g iff s |= Fax f,g ) ) iff SIGMA g is_a_fixpoint_of TransEG f )
set G = SIGMA g;
set Q = SIGMA (Fax f,g);
A1: (TransEG f) . (SIGMA g) = SigFaxTau f,(SIGMA g),R,BASSIGN by Def70
.= SIGMA (Fax f,g) by Th31 ;
A2: ( SIGMA g is_a_fixpoint_of TransEG f implies for s being Element of S holds
( s |= g iff s |= Fax f,g ) )

proof

assume SIGMA g is_a_fixpoint_of TransEG f ; :: thesis: for s being Element of S holds
( s |= g iff s |= Fax f,g )
then A3: SIGMA g = SIGMA (Fax f,g) by A1, ABIAN:def 4;
for s being Element of S holds
( s |= g iff s |= Fax f,g )

proof

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

proof

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

end;

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

end;

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

end;

( ( for s being Element of S holds
( s |= g iff s |= Fax f,g ) ) implies SIGMA g is_a_fixpoint_of TransEG f )

proof

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

proof

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

end;

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

proof

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

end;

then SIGMA g = (TransEG f) . (SIGMA g) by A1, A5, TARSKI:2;
hence SIGMA g is_a_fixpoint_of TransEG f by ABIAN:def 4; :: thesis: verum

end;

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