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 object st s in SIGMA (Fax (f,g)) holds
s in SIGMA g

proof

let x be object ; :: 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 object st x in SIGMA g holds
x in SIGMA (Fax (f,g))

proof

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