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, g be Assign of (BASSModel (R,BASSIGN)); :: thesis:
A1: for s being object holds
( s in SIGMA ('not' f) iff s in S \ (SIGMA f) )

proof

let s be object ; :: thesis:
A2: ( s in SIGMA ('not' f) implies s in S \ (SIGMA f) )

proof

assume A3: s in SIGMA ('not' f) ; :: thesis:
then A4: ex x being Element of S st
( x = s & x |= 'not' f ) ;
reconsider s = s as Element of S by A3;
not s in SIGMA f

proof

assume s in SIGMA f ; :: thesis:
then ex y being Element of S st
( y = s & y |= f ) ;
hence contradiction by A4, Th12; :: thesis:

end;

hence s in S \ (SIGMA f) by XBOOLE_0:def 5; :: thesis:

end;

( s in S \ (SIGMA f) implies s in SIGMA ('not' f) )

proof

assume A5: s in S \ (SIGMA f) ; :: thesis:
then reconsider s = s as Element of S ;
not s in SIGMA f by A5, XBOOLE_0:def 5;
then s |/= f ;
then s |= 'not' f by Th12;
hence s in SIGMA ('not' f) ; :: thesis:

end;

hence ( s in SIGMA ('not' f) iff s in S \ (SIGMA f) ) by A2; :: thesis:

end;

A6: for s being object holds
( s in SIGMA (f 'or' g) iff s in (SIGMA f) \/ (SIGMA g) )

proof

let s be object ; :: thesis:
A7: ( s in (SIGMA f) \/ (SIGMA g) implies s in SIGMA (f 'or' g) )

proof

assume A8: s in (SIGMA f) \/ (SIGMA g) ; :: thesis:

per cases by A8, XBOOLE_0:def 3;

suppose A9: s in SIGMA f ; :: thesis:

then A10: ex x being Element of S st
( x = s & x |= f ) ;
reconsider s = s as Element of S by A9;
s |= f 'or' g by A10, Th17;
hence s in SIGMA (f 'or' g) ; :: thesis:

end;

suppose A11: s in SIGMA g ; :: thesis:

then A12: ex x being Element of S st
( x = s & x |= g ) ;
reconsider s = s as Element of S by A11;
s |= f 'or' g by A12, Th17;
hence s in SIGMA (f 'or' g) ; :: thesis:

end;

end;

end;

( s in SIGMA (f 'or' g) implies s in (SIGMA f) \/ (SIGMA g) )

proof

assume A13: s in SIGMA (f 'or' g) ; :: thesis:
then A14: ex x being Element of S st
( x = s & x |= f 'or' g ) ;
reconsider s = s as Element of S by A13;

per cases by A14, Th17;

suppose s |= f ; :: thesis:

then s in SIGMA f ;
hence s in (SIGMA f) \/ (SIGMA g) by XBOOLE_0:def 3; :: thesis:

end;

suppose s |= g ; :: thesis:

then s in SIGMA g ;
hence s in (SIGMA f) \/ (SIGMA g) by XBOOLE_0:def 3; :: thesis:

end;

end;

end;

hence ( s in SIGMA (f 'or' g) iff s in (SIGMA f) \/ (SIGMA g) ) by A7; :: thesis:

end;

for s being object holds
( s in SIGMA (f '&' g) iff s in (SIGMA f) /\ (SIGMA g) )

proof

let s be object ; :: thesis:
thus ( s in SIGMA (f '&' g) implies s in (SIGMA f) /\ (SIGMA g) ) :: thesis:

proof

assume A15: s in SIGMA (f '&' g) ; :: thesis:
then A16: ex x being Element of S st
( x = s & x |= f '&' g ) ;
reconsider s = s as Element of S by A15;
s |= g by A16, Th13;
then A17: s in SIGMA g ;
s |= f by A16, Th13;
then s in SIGMA f ;
hence s in (SIGMA f) /\ (SIGMA g) by A17, XBOOLE_0:def 4; :: thesis:

end;

assume A18: s in (SIGMA f) /\ (SIGMA g) ; :: thesis:
then A19: s in SIGMA g by XBOOLE_0:def 4;
s in SIGMA f by A18, XBOOLE_0:def 4;
then A20: ex x being Element of S st
( x = s & x |= f ) ;
reconsider s = s as Element of S by A18;
ex y being Element of S st
( y = s & y |= g ) by A19;
then s |= f '&' g by A20, Th13;
hence s in SIGMA (f '&' g) ; :: thesis:

end;

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; :: thesis: