let A be Element of LTLB_WFF ; :: thesis: ( not A is conditional implies tau1 . A = {A} )
assume not A is conditional ; :: thesis: tau1 . A = {A}
then ( A is conjunctive or A is simple or A = TFALSUM ) by HILBERT2:9;
then ex r, s being Element of LTLB_WFF st
( A = r 'U' s or ex n being Element of NAT st
( A = prop n or A = TFALSUM ) ) by HILBERT2:def 8, HILBERT2:def 6;
hence tau1 . A = {A} by Def4; :: thesis: verum