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 T being Subset of S holds SIGMA (Tau (T,R,BASSIGN)) = T
let R be total Relation of S,S; :: thesis: for BASSIGN being non empty Subset of (ModelSP S)
for T being Subset of S holds SIGMA (Tau (T,R,BASSIGN)) = T
let BASSIGN be non empty Subset of (ModelSP S); :: thesis: for T being Subset of S holds SIGMA (Tau (T,R,BASSIGN)) = T
let T be Subset of S; :: thesis: SIGMA (Tau (T,R,BASSIGN)) = T
set f = Tau (T,R,BASSIGN);
set U = SIGMA (Tau (T,R,BASSIGN));
A1: SIGMA (Tau (T,R,BASSIGN)) = { s where s is Element of S : (Fid ((Tau (T,R,BASSIGN)),S)) . s = TRUE } by Lm46;
for s being set holds
( s in SIGMA (Tau (T,R,BASSIGN)) iff s in T )

proof

let s be set ; :: thesis: ( s in SIGMA (Tau (T,R,BASSIGN)) iff s in T )
thus ( s in SIGMA (Tau (T,R,BASSIGN)) implies s in T ) :: thesis: ( s in T implies s in SIGMA (Tau (T,R,BASSIGN)) )

proof

assume s in SIGMA (Tau (T,R,BASSIGN)) ; :: thesis: s in T
then ex t being Element of S st
( s = t & (Fid ((Tau (T,R,BASSIGN)),S)) . t = TRUE ) by A1;
then (chi (T,S)) . s = TRUE by Def66;
hence s in T by FUNCT_3:36; :: thesis: verum

end;

assume A2: s in T ; :: thesis: s in SIGMA (Tau (T,R,BASSIGN))
then (Fid ((Tau (T,R,BASSIGN)),S)) . s = (chi (T,S)) . s by Def66
.= 1 by A2, FUNCT_3:def 3 ;
hence s in SIGMA (Tau (T,R,BASSIGN)) by A1, A2; :: thesis: verum

end;

hence SIGMA (Tau (T,R,BASSIGN)) = T by TARSKI:1; :: thesis: verum