let H be LTL-formula; :: thesis: ( H is atomic or H is negative or H is conjunctive or H is disjunctive or H is next or H is Until or H is Release )
A1: H is Element of LTL_WFF by Def13;
assume A2: ( not H is atomic & not H is negative & not H is conjunctive & not H is disjunctive & not H is next & not H is Until & not H is Release ) ; :: thesis: contradiction
A3: not LTL_WFF \ {H} is empty

proof

A4: atom. 0 in LTL_WFF by Def12;
atom. 0 <> H by A2, Def14;
then not atom. 0 in {H} by TARSKI:def 1;
hence not LTL_WFF \ {H} is empty by A4, XBOOLE_0:def 5; :: thesis: verum

end;

A5: for a being set st a in LTL_WFF \ {H} holds
a is FinSequence of NAT by Def12;

A6: now

let n be Nat; :: thesis: atom. n in LTL_WFF \ {H}
A7: atom. n in LTL_WFF by Def12;
atom. n <> H by A2, Def14;
then not atom. n in {H} by TARSKI:def 1;
hence atom. n in LTL_WFF \ {H} by A7, XBOOLE_0:def 5; :: thesis: verum

end;

A8: now

let p be FinSequence of NAT ; :: thesis: ( p in LTL_WFF \ {H} implies 'not' p in LTL_WFF \ {H} )
assume A9: p in LTL_WFF \ {H} ; :: thesis: 'not' p in LTL_WFF \ {H}
then A10: 'not' p in LTL_WFF by Def12;
reconsider H1 = p as LTL-formula by A9, Def13;
'not' H1 <> H by A2, Def15;
then not 'not' p in {H} by TARSKI:def 1;
hence 'not' p in LTL_WFF \ {H} by A10, XBOOLE_0:def 5; :: thesis: verum

end;

A11: now

let p, q be FinSequence of NAT ; :: thesis: ( p in LTL_WFF \ {H} & q in LTL_WFF \ {H} implies p '&' q in LTL_WFF \ {H} )
assume A12: ( p in LTL_WFF \ {H} & q in LTL_WFF \ {H} ) ; :: thesis: p '&' q in LTL_WFF \ {H}
then A13: p '&' q in LTL_WFF by Def12;
reconsider F = p, G = q as LTL-formula by A12, Def13;
F '&' G <> H by A2, Def16;
then not p '&' q in {H} by TARSKI:def 1;
hence p '&' q in LTL_WFF \ {H} by A13, XBOOLE_0:def 5; :: thesis: verum

end;

A14: now

let p, q be FinSequence of NAT ; :: thesis: ( p in LTL_WFF \ {H} & q in LTL_WFF \ {H} implies p 'or' q in LTL_WFF \ {H} )
assume A15: ( p in LTL_WFF \ {H} & q in LTL_WFF \ {H} ) ; :: thesis: p 'or' q in LTL_WFF \ {H}
then A16: p 'or' q in LTL_WFF by Def12;
reconsider F = p, G = q as LTL-formula by A15, Def13;
F 'or' G <> H by A2, Def17;
then not p 'or' q in {H} by TARSKI:def 1;
hence p 'or' q in LTL_WFF \ {H} by A16, XBOOLE_0:def 5; :: thesis: verum

end;

A17: now

let p be FinSequence of NAT ; :: thesis: ( p in LTL_WFF \ {H} implies 'X' p in LTL_WFF \ {H} )
assume A18: p in LTL_WFF \ {H} ; :: thesis: 'X' p in LTL_WFF \ {H}
then A19: 'X' p in LTL_WFF by Def12;
reconsider H1 = p as LTL-formula by A18, Def13;
'X' H1 <> H by A2, Def18;
then not 'X' p in {H} by TARSKI:def 1;
hence 'X' p in LTL_WFF \ {H} by A19, XBOOLE_0:def 5; :: thesis: verum

end;

A20: now

let p, q be FinSequence of NAT ; :: thesis: ( p in LTL_WFF \ {H} & q in LTL_WFF \ {H} implies p 'U' q in LTL_WFF \ {H} )
assume A21: ( p in LTL_WFF \ {H} & q in LTL_WFF \ {H} ) ; :: thesis: p 'U' q in LTL_WFF \ {H}
then A22: p 'U' q in LTL_WFF by Def12;
reconsider F = p, G = q as LTL-formula by A21, Def13;
F 'U' G <> H by A2, Def19;
then not p 'U' q in {H} by TARSKI:def 1;
hence p 'U' q in LTL_WFF \ {H} by A22, XBOOLE_0:def 5; :: thesis: verum

end;

now

let p, q be FinSequence of NAT ; :: thesis: ( p in LTL_WFF \ {H} & q in LTL_WFF \ {H} implies p 'R' q in LTL_WFF \ {H} )
assume A23: ( p in LTL_WFF \ {H} & q in LTL_WFF \ {H} ) ; :: thesis: p 'R' q in LTL_WFF \ {H}
then A24: p 'R' q in LTL_WFF by Def12;
reconsider F = p, G = q as LTL-formula by A23, Def13;
F 'R' G <> H by A2, Def1901;
then not p 'R' q in {H} by TARSKI:def 1;
hence p 'R' q in LTL_WFF \ {H} by A24, XBOOLE_0:def 5; :: thesis: verum

end;

then LTL_WFF c= LTL_WFF \ {H} by A3, A5, A6, A8, A11, A14, A17, A20, Def12;
then H in LTL_WFF \ {H} by A1, TARSKI:def 3;
then ( not H in {H} & H in {H} ) by TARSKI:def 1, XBOOLE_0:def 5;
hence contradiction ; :: thesis: verum