let A be Element of LTLB_WFF ; :: thesis: for n being Element of NAT
for M being LTLModel holds
( (SAT M) . [n,('not' A)] = 1 iff (SAT M) . [n,A] = 0 )
let n be Element of NAT ; :: thesis: for M being LTLModel holds
( (SAT M) . [n,('not' A)] = 1 iff (SAT M) . [n,A] = 0 )
let M be LTLModel; :: thesis: ( (SAT M) . [n,('not' A)] = 1 iff (SAT M) . [n,A] = 0 )

hereby :: thesis: ( (SAT M) . [n,A] = 0 implies (SAT M) . [n,('not' A)] = 1 )

assume (SAT M) . [n,('not' A)] = 1 ; :: thesis: (SAT M) . [n,A] = 0
then A1: ((SAT M) . [n,A]) => ((SAT M) . [n,TFALSUM]) = 1 by Def11;
( (SAT M) . [n,A] = 1 or (SAT M) . [n,A] = 0 ) by XBOOLEAN:def 3;
hence (SAT M) . [n,A] = 0 by A1, Def11; :: thesis: verum

end;

assume A2: (SAT M) . [n,A] = 0 ; :: thesis: (SAT M) . [n,('not' A)] = 1
thus (SAT M) . [n,('not' A)] = ((SAT M) . [n,A]) => ((SAT M) . [n,TFALSUM]) by Def11
.= 1 by A2 ; :: thesis: verum