theorem Th65: :: MODELC_2:65

for H1, H2 being LTL-formula
for r being Element of Inf_seq AtomicFamily holds
( r |= H1 '&' H2 iff ( r |= H1 & r |= H2 ) )