let B be Element of LTLB_WFF ; :: thesis: for n being Element of NAT
for M being LTLModel holds (SAT M) . [n,(('not' ('X' B)) => ('X' ('not' B)))] = 1
let n be Element of NAT ; :: thesis: for M being LTLModel holds (SAT M) . [n,(('not' ('X' B)) => ('X' ('not' B)))] = 1
let M be LTLModel; :: thesis: (SAT M) . [n,(('not' ('X' B)) => ('X' ('not' B)))] = 1
A1: ( (SAT M) . [n,('not' ('X' B))] = 0 or (SAT M) . [n,('not' ('X' B))] = 1 ) by XBOOLEAN:def 3;
thus (SAT M) . [n,(('not' ('X' B)) => ('X' ('not' B)))] = ((SAT M) . [n,('not' ('X' B))]) => ((SAT M) . [n,('X' ('not' B))]) by Def11
.= 1 by A1, Th14 ; :: thesis: verum