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 Def10;
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
then atom. 0 <> H ;
then A3: not atom. 0 in {H} by TARSKI:def 1;

A4: now :: thesis: for p, q being FinSequence of NAT st p in LTL_WFF \ {H} & q in LTL_WFF \ {H} holds
p 'R' q in LTL_WFF \ {H}

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 A5: ( p in LTL_WFF \ {H} & q in LTL_WFF \ {H} ) ; :: thesis: p 'R' q in LTL_WFF \ {H}
then reconsider F = p, G = q as LTL-formula by Def10;
F 'R' G <> H by A2;
then A6: not p 'R' q in {H} by TARSKI:def 1;
p 'R' q in LTL_WFF by A5, Def9;
hence p 'R' q in LTL_WFF \ {H} by A6, XBOOLE_0:def 5; :: thesis: verum

end;

A7: now :: thesis: for p, q being FinSequence of NAT st p in LTL_WFF \ {H} & q in LTL_WFF \ {H} holds
p 'U' q in LTL_WFF \ {H}

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 A8: ( p in LTL_WFF \ {H} & q in LTL_WFF \ {H} ) ; :: thesis: p 'U' q in LTL_WFF \ {H}
then reconsider F = p, G = q as LTL-formula by Def10;
F 'U' G <> H by A2;
then A9: not p 'U' q in {H} by TARSKI:def 1;
p 'U' q in LTL_WFF by A8, Def9;
hence p 'U' q in LTL_WFF \ {H} by A9, XBOOLE_0:def 5; :: thesis: verum

end;

A10: now :: thesis: for p being FinSequence of NAT st p in LTL_WFF \ {H} holds
'X' p in LTL_WFF \ {H}

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

end;

A13: now :: thesis: for p, q being FinSequence of NAT st p in LTL_WFF \ {H} & q in LTL_WFF \ {H} holds
p 'or' q in LTL_WFF \ {H}

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 A14: ( p in LTL_WFF \ {H} & q in LTL_WFF \ {H} ) ; :: thesis: p 'or' q in LTL_WFF \ {H}
then reconsider F = p, G = q as LTL-formula by Def10;
F 'or' G <> H by A2;
then A15: not p 'or' q in {H} by TARSKI:def 1;
p 'or' q in LTL_WFF by A14, Def9;
hence p 'or' q in LTL_WFF \ {H} by A15, XBOOLE_0:def 5; :: thesis: verum

end;

A16: now :: thesis: for p, q being FinSequence of NAT st p in LTL_WFF \ {H} & q in LTL_WFF \ {H} holds
p '&' q in LTL_WFF \ {H}

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 A17: ( p in LTL_WFF \ {H} & q in LTL_WFF \ {H} ) ; :: thesis: p '&' q in LTL_WFF \ {H}
then reconsider F = p, G = q as LTL-formula by Def10;
F '&' G <> H by A2;
then A18: not p '&' q in {H} by TARSKI:def 1;
p '&' q in LTL_WFF by A17, Def9;
hence p '&' q in LTL_WFF \ {H} by A18, XBOOLE_0:def 5; :: thesis: verum

end;

A19: now :: thesis: for p being FinSequence of NAT st p in LTL_WFF \ {H} holds
'not' p in LTL_WFF \ {H}

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

end;

A22: now :: thesis: for n being Nat holds atom. n in LTL_WFF \ {H}

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

end;

atom. 0 in LTL_WFF by Def9;
then A24: not LTL_WFF \ {H} is empty by A3, XBOOLE_0:def 5;
for a being set st a in LTL_WFF \ {H} holds
a is FinSequence of NAT by Def9;
then LTL_WFF c= LTL_WFF \ {H} by A24, A22, A19, A16, A13, A10, A7, A4, Def9;
then H in LTL_WFF \ {H} by A1;
then not H in {H} by XBOOLE_0:def 5;
hence contradiction by TARSKI:def 1; :: thesis: verum