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 Th6;
hence contradiction by Def12; :: thesis: verum