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 consider t being Element of S such that
A2: s = t and
A3: (Fid (Tau T,R,BASSIGN),S) . t = TRUE by A1;
(chi T,S) . s = TRUE by A2, A3, Def64;
hence s in T by FUNCT_3:42; :: thesis: verum

end;

assume A4: 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 A4, FUNCT_3:def 3 ;
hence s in SIGMA (Tau T,R,BASSIGN) by A1, A4; :: thesis: verum

end;

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