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

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