let A be Element of LTLB_WFF ; :: thesis: ( {} LTLB_WFF |= A iff not 'not' A is satisfiable )

hereby :: thesis: ( not 'not' A is satisfiable implies {} LTLB_WFF |= A )

assume A1: {} LTLB_WFF |= A ; :: thesis: not 'not' A is satisfiable
assume 'not' A is satisfiable ; :: thesis: contradiction
then consider M being LTLModel, n being Element of NAT such that
A2: (SAT M) . [n,('not' A)] = 1 ;
A3: M |= {} LTLB_WFF ;
(SAT M) . [n,A] = 0 by A2, LTLAXIO1:5;
hence contradiction by A3, A1, LTLAXIO1:def 12; :: thesis: verum

end;

assume A4: not 'not' A is satisfiable ; :: thesis: {} LTLB_WFF |= A
assume not {} LTLB_WFF |= A ; :: thesis: contradiction
then consider M being LTLModel such that
M |= {} LTLB_WFF and
A5: not M |= A ;
consider n being Element of NAT such that
A6: not (SAT M) . [n,A] = 1 by A5;
(SAT M) . [n,('not' A)] = 1 by A6, XBOOLEAN:def 3, LTLAXIO1:5;
hence contradiction by A4; :: thesis: verum