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 being Assign of (BASSModel (R,BASSIGN)) holds SIGMA (EX f) = Pred ((SIGMA f),R)
let R be total Relation of S,S; :: thesis: for BASSIGN being non empty Subset of (ModelSP S)
for f being Assign of (BASSModel (R,BASSIGN)) holds SIGMA (EX f) = Pred ((SIGMA f),R)
let BASSIGN be non empty Subset of (ModelSP S); :: thesis: for f being Assign of (BASSModel (R,BASSIGN)) holds SIGMA (EX f) = Pred ((SIGMA f),R)
let f be Assign of (BASSModel (R,BASSIGN)); :: thesis: SIGMA (EX f) = Pred ((SIGMA f),R)
set g = EX f;
set H = SIGMA f;
A1: for x being object st x in Pred ((SIGMA f),R) holds
x in SIGMA (EX f)

proof

let x be object ; :: thesis: ( x in Pred ((SIGMA f),R) implies x in SIGMA (EX f) )
assume x in Pred ((SIGMA f),R) ; :: thesis: x in SIGMA (EX f)
then consider s being Element of S such that
A2: x = s and
A3: ex s1 being Element of S st
( s1 in SIGMA f & [s,s1] in R ) ;
consider s1 being Element of S such that
A4: s1 in SIGMA f and
A5: [s,s1] in R by A3;
ex s2 being Element of S st
( s1 = s2 & s2 |= f ) by A4;
then s |= EX f by A5, Th28;
hence x in SIGMA (EX f) by A2; :: thesis: verum

end;

for x being object st x in SIGMA (EX f) holds
x in Pred ((SIGMA f),R)

proof

let x be object ; :: thesis: ( x in SIGMA (EX f) implies x in Pred ((SIGMA f),R) )
assume x in SIGMA (EX f) ; :: thesis: x in Pred ((SIGMA f),R)
then consider s being Element of S such that
A6: x = s and
A7: s |= EX f ;
consider s1 being Element of S such that
A8: [s,s1] in R and
A9: s1 |= f by A7, Th28;
s1 in SIGMA f by A9;
hence x in Pred ((SIGMA f),R) by A6, A8; :: thesis: verum

end;

hence SIGMA (EX f) = Pred ((SIGMA f),R) by A1, TARSKI:2; :: thesis: verum