let A be Element of LTLB_WFF ; :: thesis: ( TVERUM '&&' A is satisfiable implies A is satisfiable )
assume TVERUM '&&' A is satisfiable ; :: thesis: A is satisfiable
then consider M being LTLModel, n being Element of NAT such that
A1: (SAT M) . [n,(TVERUM '&&' A)] = 1 ;
(SAT M) . [n,A] = 1 by LTLAXIO1:7, A1;
hence A is satisfiable ; :: thesis: verum