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 (CTLModel 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 (CTLModel 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 (CTLModel 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 (CTLModel 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 set holds
( s in SIGMA ('not' f) iff s in S \ (SIGMA f) )

proof

let s be set ; :: 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 s in SIGMA ('not' f) ; :: thesis: s in S \ (SIGMA f)
then consider x being Element of S such that
A3: x = s and
A4: 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 consider y being Element of S such that
A5: y = s and
A6: y |= f ;
thus contradiction by A3, A4, A5, A6, 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 A7: 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 A7, 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;

A8: for s being set holds
( s in SIGMA (f '&' g) iff s in (SIGMA f) /\ (SIGMA g) )

proof

let s be set ; :: 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 s in SIGMA (f '&' g) ; :: thesis: s in (SIGMA f) /\ (SIGMA g)
then consider x being Element of S such that
A9: x = s and
A10: x |= f '&' g ;
reconsider s = s as Element of S by A9;
A11: ( s |= f & s |= g ) by A9, A10, Th13;
then A12: s in SIGMA f ;
s in SIGMA g by A11;
hence s in (SIGMA f) /\ (SIGMA g) by A12, XBOOLE_0:def 4; :: thesis: verum

end;

assume s in (SIGMA f) /\ (SIGMA g) ; :: thesis: s in SIGMA (f '&' g)
then A13: ( s in SIGMA f & s in SIGMA g ) by XBOOLE_0:def 4;
then consider x being Element of S such that
A14: x = s and
A15: x |= f ;
reconsider s = s as Element of S by A14;
consider y being Element of S such that
A16: y = s and
A17: y |= g by A13;
s |= f '&' g by A14, A15, A16, A17, Th13;
hence s in SIGMA (f '&' g) ; :: thesis: verum

end;

for s being set holds
( s in SIGMA (f 'or' g) iff s in (SIGMA f) \/ (SIGMA g) )

proof

let s be set ; :: thesis: ( s in SIGMA (f 'or' g) iff s in (SIGMA f) \/ (SIGMA g) )
A18: ( s in SIGMA (f 'or' g) implies s in (SIGMA f) \/ (SIGMA g) )

proof

assume s in SIGMA (f 'or' g) ; :: thesis: s in (SIGMA f) \/ (SIGMA g)
then consider x being Element of S such that
A19: x = s and
A20: x |= f 'or' g ;
reconsider s = s as Element of S by A19;

per cases ( s |= f or s |= g ) by A19, A20, 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;

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

proof

assume A21: 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 A21, XBOOLE_0:def 3;

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

then consider x being Element of S such that
A22: x = s and
A23: x |= f ;
reconsider s = s as Element of S by A22;
s |= f 'or' g by A22, A23, Th17;
hence s in SIGMA (f 'or' g) ; :: thesis: verum

end;

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

then consider x being Element of S such that
A24: x = s and
A25: x |= g ;
reconsider s = s as Element of S by A24;
s |= f 'or' g by A24, A25, Th17;
hence s in SIGMA (f 'or' g) ; :: thesis: verum

end;

end;

end;

hence ( s in SIGMA (f 'or' g) iff s in (SIGMA f) \/ (SIGMA g) ) by A18; :: 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, A8, TARSKI:2; :: thesis: verum