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, 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; :: thesis: 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); :: thesis: 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)); :: thesis: ( 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) )

proof

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

proof

assume A3: s in SIGMA ('not' f) ; :: thesis: s in S \ (SIGMA f)
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: contradiction
then ex y being Element of S st
( y = s & y |= f ) ;
hence contradiction by A4, Th12; :: thesis: verum

end;

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

end;

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

proof

assume A5: s in S \ (SIGMA f) ; :: thesis: s in SIGMA ('not' f)
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: verum

end;

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

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: ( s in SIGMA (f 'or' g) iff s in (SIGMA f) \/ (SIGMA g) )
A7: ( s in (SIGMA f) \/ (SIGMA g) implies s in SIGMA (f 'or' g) )

proof

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

per cases ( s in SIGMA f or s in SIGMA g ) by A8, XBOOLE_0:def 3;

suppose A9: s in SIGMA f ; :: thesis: s in SIGMA (f 'or' g)

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: verum

end;

suppose A11: s in SIGMA g ; :: thesis: s in SIGMA (f 'or' g)

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: verum

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: s in (SIGMA f) \/ (SIGMA g)
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 ( s |= f or s |= g ) by A14, Th17;

suppose s |= f ; :: thesis: s in (SIGMA f) \/ (SIGMA g)

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

end;

suppose s |= g ; :: thesis: s in (SIGMA f) \/ (SIGMA g)

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

end;

end;

end;

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

end;

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

proof

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

proof

assume A15: s in SIGMA (f '&' g) ; :: thesis: s in (SIGMA f) /\ (SIGMA g)
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: verum

end;

assume A18: s in (SIGMA f) /\ (SIGMA g) ; :: thesis: s in SIGMA (f '&' g)
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: verum

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: verum