let F be non empty finite Subset of LTLB_WFF; :: thesis: ex p being Element of LTLB_WFF st
( p in tau F & tau ((tau F) \ {p}) = (tau F) \ {p} )
set G = { A where A is Element of LTLB_WFF : ( A in tau F & A is conditional ) } ;
A1: { A where A is Element of LTLB_WFF : ( A in tau F & A is conditional ) } c= tau F

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { A where A is Element of LTLB_WFF : ( A in tau F & A is conditional ) } or x in tau F )
assume x in { A where A is Element of LTLB_WFF : ( A in tau F & A is conditional ) } ; :: thesis: x in tau F
then ex A being Element of LTLB_WFF st
( A = x & A in tau F & A is conditional ) ;
hence x in tau F ; :: thesis: verum

end;

A2: { A where A is Element of LTLB_WFF : ( A in tau F & A is conditional ) } is FinSequenceSet of NAT

proof

let x be object ; :: according to FINSEQ_2:def 3 :: thesis: ( not x in { A where A is Element of LTLB_WFF : ( A in tau F & A is conditional ) } or x is FinSequence of NAT )
assume x in { A where A is Element of LTLB_WFF : ( A in tau F & A is conditional ) } ; :: thesis: x is FinSequence of NAT
then ex A being Element of LTLB_WFF st
( A = x & A in tau F & A is conditional ) ;
hence x is FinSequence of NAT by Th2; :: thesis: verum

end;

per cases ( { A where A is Element of LTLB_WFF : ( A in tau F & A is conditional ) } = {} or { A where A is Element of LTLB_WFF : ( A in tau F & A is conditional ) } <> {} ) ;

suppose A3: { A where A is Element of LTLB_WFF : ( A in tau F & A is conditional ) } = {} ; :: thesis: ex p being Element of LTLB_WFF st
( p in tau F & tau ((tau F) \ {p}) = (tau F) \ {p} )

A4: F is without_implication

proof

assume not F is without_implication ; :: thesis: contradiction
then consider p being Element of LTLB_WFF such that
A5: ( p in F & p is conditional ) ;
F c= tau F by LTLAXIO3:16;
then p in { A where A is Element of LTLB_WFF : ( A in tau F & A is conditional ) } by A5;
hence contradiction by A3; :: thesis: verum

end;

consider p being object such that
A6: p in F by XBOOLE_0:def 1;
reconsider p = p as Element of LTLB_WFF by A6;
set Fp = (tau F) \ {p};
(tau F) \ {p} c= tau F by XBOOLE_1:36;
then A7: (tau F) \ {p} c= F by LTLAXIO3:18, A4;
A8: tau ((tau F) \ {p}) c= (tau F) \ {p}

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in tau ((tau F) \ {p}) or x in (tau F) \ {p} )
assume x in tau ((tau F) \ {p}) ; :: thesis: x in (tau F) \ {p}
then consider A being Element of LTLB_WFF such that
A9: A in (tau F) \ {p} and
A10: x in tau1 . A by LTLAXIO3:def 5;
x in {A} by A7, A9, A4, A10, LTLAXIO3:5;
hence x in (tau F) \ {p} by TARSKI:def 1, A9; :: thesis: verum

end;

( (tau F) \ {p} c= tau ((tau F) \ {p}) & p in tau F ) by LTLAXIO3:16, A4, A6, LTLAXIO3:18;
hence ex p being Element of LTLB_WFF st
( p in tau F & tau ((tau F) \ {p}) = (tau F) \ {p} ) by A8, XBOOLE_0:def 10; :: thesis: verum

end;

suppose { A where A is Element of LTLB_WFF : ( A in tau F & A is conditional ) } <> {} ; :: thesis: ex p being Element of LTLB_WFF st
( p in tau F & tau ((tau F) \ {p}) = (tau F) \ {p} )

then reconsider G = { A where A is Element of LTLB_WFF : ( A in tau F & A is conditional ) } as non empty finite FinSequenceSet of NAT by A2, A1;
consider A being FinSequence such that
A11: A in G and
A12: for B being FinSequence st B in G holds
len B <= len A by Th1;
set Fp = (tau F) \ {A};
A13: (tau F) \ {A} c= tau F by XBOOLE_1:36;
A14: tau ((tau F) \ {A}) c= (tau F) \ {A}

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in tau ((tau F) \ {A}) or x in (tau F) \ {A} )
assume x in tau ((tau F) \ {A}) ; :: thesis: x in (tau F) \ {A}
then consider p being Element of LTLB_WFF such that
A15: p in (tau F) \ {A} and
A16: x in tau1 . p by LTLAXIO3:def 5;
A17: not p in {A} by XBOOLE_0:def 5, A15;
then A18: p <> A by TARSKI:def 1;
x <> A

proof

per cases ( p is conditional or not p is conditional ) ;

suppose p is conditional ; :: thesis: x <> A

then p in G by A15, A13;
then A19: len A >= len p by A12;

per cases ( x = p or x <> p ) ;

suppose x = p ; :: thesis: x <> A

hence x <> A by A17, TARSKI:def 1; :: thesis: verum

end;

suppose x <> p ; :: thesis: x <> A

hence x <> A by LTLAXIO3:11, A16, A19; :: thesis: verum

end;

end;

end;

suppose not p is conditional ; :: thesis: x <> A

then x in {p} by LTLAXIO3:5, A16;
hence x <> A by TARSKI:def 1, A18; :: thesis: verum

end;

end;

end;

then A20: not x in {A} by TARSKI:def 1;
tau1 . p c= tau F by LTLAXIO3:23, A15, A13;
hence x in (tau F) \ {A} by A20, XBOOLE_0:def 5, A16; :: thesis: verum
reconsider x1 = x as Element of LTLB_WFF by A16;

end;

( (tau F) \ {A} c= tau ((tau F) \ {A}) & ex q being Element of LTLB_WFF st
( q = A & q in tau F & q is conditional ) ) by LTLAXIO3:16, A11;
hence ex p being Element of LTLB_WFF st
( p in tau F & tau ((tau F) \ {p}) = (tau F) \ {p} ) by A14, XBOOLE_0:def 10; :: thesis: verum

end;

end;