let n be Element of NAT ; :: thesis: for M being LTLModel holds (SAT M) . [n,TVERUM] = 1
let M be LTLModel; :: thesis: (SAT M) . [n,TVERUM] = 1
assume not (SAT M) . [n,TVERUM] = 1 ; :: thesis: contradiction
then not (SAT M) . [n,TFALSUM] = 0 by Th5;
hence contradiction by Def11; :: thesis: verum