theorem Th7: :: LTLAXIO1:7

for A, B being Element of LTLB_WFF
for n being Element of NAT
for M being LTLModel holds
( (SAT M) . [n,(A '&&' B)] = 1 iff ( (SAT M) . [n,A] = 1 & (SAT M) . [n,B] = 1 ) )