let S be non empty set ; 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; 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); for f being Assign of (BASSModel (R,BASSIGN)) holds SIGMA (EX f) = Pred ((SIGMA f),R)
let f be Assign of (BASSModel (R,BASSIGN)); 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)
for x being object st x in SIGMA (EX f) holds
x in Pred ((SIGMA f),R)
hence
SIGMA (EX f) = Pred ((SIGMA f),R)
by A1, TARSKI:2; verum