let p, q be Element of LTLB_WFF ; :: thesis: for X being Subset of LTLB_WFF st X |- p => (q '&&' ('not' q)) holds
X |- 'not' p
let X be Subset of LTLB_WFF; :: thesis: ( X |- p => (q '&&' ('not' q)) implies X |- 'not' p )
(p => (q '&&' ('not' q))) => ('not' p) is ctaut by Th43;
then (p => (q '&&' ('not' q))) => ('not' p) in LTL_axioms by LTLAXIO1:def 17;
then A1: X |- (p => (q '&&' ('not' q))) => ('not' p) by LTLAXIO1:42;
assume X |- p => (q '&&' ('not' q)) ; :: thesis: X |- 'not' p
hence X |- 'not' p by A1, LTLAXIO1:43; :: thesis: verum