let S be non empty set ; :: thesis:
let R be total Relation of S,S; :: thesis:
let BASSIGN be non empty Subset of (ModelSP S); :: thesis:
let f be Assign of (BASSModel (R,BASSIGN)); :: thesis:
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)

let x be object ; :: thesis:
assume x in Pred ((SIGMA f),R) ; :: thesis:
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:

end;

let x be object ; :: thesis:
assume x in SIGMA (EX f) ; :: thesis:
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:

end;