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 Def64;
hence s in T by FUNCT_3:42; :: 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 Def64
.= 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:2; :: thesis: verum