let A be Element of LTLB_WFF ; :: thesis: for P being consistent PNPair holds
( A in rng P or [((P `1) ^^ <*A*>),(P `2)] is consistent or [(P `1),((P `2) ^^ <*A*>)] is consistent )
let P be consistent PNPair; :: thesis: ( A in rng P or [((P `1) ^^ <*A*>),(P `2)] is consistent or [(P `1),((P `2) ^^ <*A*>)] is consistent )
set fpa = (P `1) ^^ <*A*>;
set fma = (P `2) ^^ <*A*>;
set Pl = [((P `1) ^^ <*A*>),(P `2)];
set Pr = [(P `1),((P `2) ^^ <*A*>)];
set np = 'not' (P ^);
set npl = 'not' ([((P `1) ^^ <*A*>),(P `2)] ^);
set npr = 'not' ([(P `1),((P `2) ^^ <*A*>)] ^);
set na = <*('not' A)*>;
assume A1: not A in rng P ; :: thesis: ( [((P `1) ^^ <*A*>),(P `2)] is consistent or [(P `1),((P `2) ^^ <*A*>)] is consistent )
then not A in rng (P `1) by XBOOLE_0:def 3;
then rng (P `1) misses {A} by ZFMISC_1:50;
then rng (P `1) misses rng <*A*> by FINSEQ_1:39;
then A2: (P `1) ^^ <*A*> = (P `1) ^ <*A*> by Def3;
not A in rng (P `2) by A1, XBOOLE_0:def 3;
then rng (P `2) misses {A} by ZFMISC_1:50;
then rng (P `2) misses rng <*A*> by FINSEQ_1:39;
then (P `2) ^^ <*A*> = (P `2) ^ <*A*> by Def3;
then A3: nega ((P `2) ^^ <*A*>) = (nega (P `2)) ^ <*('not' A)*> by LTLAXIO2:15;
('not' ([((P `1) ^^ <*A*>),(P `2)] ^)) => (('not' ([(P `1),((P `2) ^^ <*A*>)] ^)) => ('not' (P ^))) is ctaut

proof

let g be Function of LTLB_WFF,BOOLEAN; :: according to LTLAXIO1:def 16 :: thesis: (VAL g) . (('not' ([((P `1) ^^ <*A*>),(P `2)] ^)) => (('not' ([(P `1),((P `2) ^^ <*A*>)] ^)) => ('not' (P ^)))) = 1
set v = VAL g;
set vf = (VAL g) . TFALSUM;
A4: (VAL g) . TFALSUM = 0 by LTLAXIO1:def 15;
set p = (((VAL g) . (P ^)) '&' ((VAL g) . A)) => ((VAL g) . TFALSUM);
set q = (((VAL g) . (P ^)) '&' (((VAL g) . A) => ((VAL g) . TFALSUM))) => ((VAL g) . TFALSUM);
A5: ( (VAL g) . A = 1 or (VAL g) . A = 0 ) by XBOOLEAN:def 3;
A6: (VAL g) . ([(P `1),((P `2) ^^ <*A*>)] ^) = ((VAL g) . H₂(P `1 )) '&' ((VAL g) . H<sub>2</sub>( nega ((P `2) ^^ <*A*>))) by LTLAXIO1:31
.= ((VAL g) . H₂(P `1 )) '&' (((VAL g) . H<sub>2</sub>( nega (P `2))) '&' ((VAL g) . H₂(<*('not' A)*>))) by LTLAXIO2:17, A3
.= (((VAL g) . H₂(P `1 )) '&' ((VAL g) . H<sub>2</sub>( nega (P `2)))) '&' ((VAL g) . H₂(<*('not' A)*>))
.= ((VAL g) . (P ^)) '&' ((VAL g) . H₂(<*('not' A)*>)) by LTLAXIO1:31
.= ((VAL g) . (P ^)) '&' ((VAL g) . ('not' A)) by LTLAXIO2:11
.= ((VAL g) . (P ^)) '&' (((VAL g) . A) => ((VAL g) . TFALSUM)) by LTLAXIO1:def 15 ;
A7: (VAL g) . ([((P `1) ^^ <*A*>),(P `2)] ^) = ((VAL g) . H₂((P `1) ^^ <*A*>)) '&' ((VAL g) . H<sub>2</sub>( nega (P `2))) by LTLAXIO1:31
.= (((VAL g) . H₂(P `1 )) '&' ((VAL g) . H<sub>2</sub>(<*A*>))) '&' ((VAL g) . H<sub>2</sub>( nega (P `2))) by LTLAXIO2:17, A2
.= (((VAL g) . H₂(P `1 )) '&' ((VAL g) . A)) '&' ((VAL g) . H<sub>2</sub>( nega (P `2))) by LTLAXIO2:11
.= (((VAL g) . H₂(P `1 )) '&' ((VAL g) . H<sub>2</sub>( nega (P `2)))) '&' ((VAL g) . A)
.= ((VAL g) . (P ^)) '&' ((VAL g) . A) by LTLAXIO1:31 ;
A8: ( (VAL g) . (P ^) = 1 or (VAL g) . (P ^) = 0 ) by XBOOLEAN:def 3;
thus (VAL g) . (('not' ([((P `1) ^^ <*A*>),(P `2)] ^)) => (('not' ([(P `1),((P `2) ^^ <*A*>)] ^)) => ('not' (P ^)))) = ((VAL g) . ('not' ([((P `1) ^^ <*A*>),(P `2)] ^))) => ((VAL g) . (('not' ([(P `1),((P `2) ^^ <*A*>)] ^)) => ('not' (P ^)))) by LTLAXIO1:def 15
.= ((VAL g) . ('not' ([((P `1) ^^ <*A*>),(P `2)] ^))) => (((VAL g) . ('not' ([(P `1),((P `2) ^^ <*A*>)] ^))) => ((VAL g) . ('not' (P ^)))) by LTLAXIO1:def 15
.= ((((VAL g) . (P ^)) '&' ((VAL g) . A)) => ((VAL g) . TFALSUM)) => (((VAL g) . ('not' ([(P `1),((P `2) ^^ <*A*>)] ^))) => ((VAL g) . ('not' (P ^)))) by A7, LTLAXIO1:def 15
.= ((((VAL g) . (P ^)) '&' ((VAL g) . A)) => ((VAL g) . TFALSUM)) => (((((VAL g) . (P ^)) '&' (((VAL g) . A) => ((VAL g) . TFALSUM))) => ((VAL g) . TFALSUM)) => ((VAL g) . ('not' (P ^)))) by A6, LTLAXIO1:def 15
.= 1 by A8, A5, A4, LTLAXIO1:def 15 ; :: thesis: verum

end;

then ('not' ([((P `1) ^^ <*A*>),(P `2)] ^)) => (('not' ([(P `1),((P `2) ^^ <*A*>)] ^)) => ('not' (P ^))) in LTL_axioms by LTLAXIO1:def 17;
then A9: {} LTLB_WFF |- ('not' ([((P `1) ^^ <*A*>),(P `2)] ^)) => (('not' ([(P `1),((P `2) ^^ <*A*>)] ^)) => ('not' (P ^))) by LTLAXIO1:42;
assume that
A10: [((P `1) ^^ <*A*>),(P `2)] is Inconsistent and
A11: [(P `1),((P `2) ^^ <*A*>)] is Inconsistent ; :: thesis: contradiction
{} LTLB_WFF |- 'not' ([((P `1) ^^ <*A*>),(P `2)] ^) by A10;
then A12: {} LTLB_WFF |- ('not' ([(P `1),((P `2) ^^ <*A*>)] ^)) => ('not' (P ^)) by A9, LTLAXIO1:43;
{} LTLB_WFF |- 'not' ([(P `1),((P `2) ^^ <*A*>)] ^) by A11;
hence contradiction by A12, Def10, LTLAXIO1:43; :: thesis: verum