theorem Th4: :: LTLAXIO1:4

for A being Element of LTLB_WFF holds
( A = TFALSUM or ex n being Element of NAT st
( A = prop n or ex p, q being Element of LTLB_WFF st
( A = p => q or ex p, q being Element of LTLB_WFF st A = p 'U' q ) ) )