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, g being Assign of (BASSModel (R,BASSIGN)) holds
( SIGMA ('not' f) = S \ (SIGMA f) & SIGMA (f '&' g) = (SIGMA f) /\ (SIGMA g) & SIGMA (f 'or' g) = (SIGMA f) \/ (SIGMA g) )
let R be total Relation of S,S; for BASSIGN being non empty Subset of (ModelSP S)
for f, g being Assign of (BASSModel (R,BASSIGN)) holds
( SIGMA ('not' f) = S \ (SIGMA f) & SIGMA (f '&' g) = (SIGMA f) /\ (SIGMA g) & SIGMA (f 'or' g) = (SIGMA f) \/ (SIGMA g) )
let BASSIGN be non empty Subset of (ModelSP S); for f, g being Assign of (BASSModel (R,BASSIGN)) holds
( SIGMA ('not' f) = S \ (SIGMA f) & SIGMA (f '&' g) = (SIGMA f) /\ (SIGMA g) & SIGMA (f 'or' g) = (SIGMA f) \/ (SIGMA g) )
let f, g be Assign of (BASSModel (R,BASSIGN)); ( SIGMA ('not' f) = S \ (SIGMA f) & SIGMA (f '&' g) = (SIGMA f) /\ (SIGMA g) & SIGMA (f 'or' g) = (SIGMA f) \/ (SIGMA g) )
A1:
for s being object holds
( s in SIGMA ('not' f) iff s in S \ (SIGMA f) )
A6:
for s being object holds
( s in SIGMA (f 'or' g) iff s in (SIGMA f) \/ (SIGMA g) )
for s being object holds
( s in SIGMA (f '&' g) iff s in (SIGMA f) /\ (SIGMA g) )
hence
( SIGMA ('not' f) = S \ (SIGMA f) & SIGMA (f '&' g) = (SIGMA f) /\ (SIGMA g) & SIGMA (f 'or' g) = (SIGMA f) \/ (SIGMA g) )
by A1, A6, TARSKI:2; verum