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 f = { s where s is Element of S : (Fid (f,S)) . s = TRUE }
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 f = { s where s is Element of S : (Fid (f,S)) . s = TRUE }
let BASSIGN be non empty Subset of (ModelSP S); :: thesis: for f being Assign of (BASSModel (R,BASSIGN)) holds SIGMA f = { s where s is Element of S : (Fid (f,S)) . s = TRUE }
let f be Assign of (BASSModel (R,BASSIGN)); :: thesis: SIGMA f = { s where s is Element of S : (Fid (f,S)) . s = TRUE }
A1: for x being object st x in { s where s is Element of S : (Fid (f,S)) . s = TRUE } holds
x in SIGMA f
proof
let x be object ; :: thesis: ( x in { s where s is Element of S : (Fid (f,S)) . s = TRUE } implies x in SIGMA f )
assume x in { s where s is Element of S : (Fid (f,S)) . s = TRUE } ; :: thesis: x in SIGMA f
then consider s being Element of S such that
A2: x = s and
A3: (Fid (f,S)) . s = TRUE ;
s |= f by A3;
hence x in SIGMA f by A2; :: thesis: verum
end;
for x being object st x in SIGMA f holds
x in { s where s is Element of S : (Fid (f,S)) . s = TRUE }
proof
let x be object ; :: thesis: ( x in SIGMA f implies x in { s where s is Element of S : (Fid (f,S)) . s = TRUE } )
assume x in SIGMA f ; :: thesis: x in { s where s is Element of S : (Fid (f,S)) . s = TRUE }
then consider s being Element of S such that
A4: x = s and
A5: s |= f ;
(Fid (f,S)) . s = TRUE by A5;
hence x in { s where s is Element of S : (Fid (f,S)) . s = TRUE } by A4; :: thesis: verum
end;
hence SIGMA f = { s where s is Element of S : (Fid (f,S)) . s = TRUE } by A1, TARSKI:2; :: thesis: verum