let p, q be Element of LTLB_WFF ; :: thesis: for X being Subset of LTLB_WFF st X |- p => q holds
X |- ('not' q) => ('not' p)
let X be Subset of LTLB_WFF; :: thesis: ( X |- p => q implies X |- ('not' q) => ('not' p) )
set A = (p => q) => (('not' q) => ('not' p));

now :: thesis: for f being Function of LTLB_WFF,BOOLEAN holds (VAL f) . ((p => q) => (('not' q) => ('not' p))) = 1

let f be Function of LTLB_WFF,BOOLEAN; :: thesis: (VAL f) . ((p => q) => (('not' q) => ('not' p))) = 1
A1: ( (VAL f) . p = 0 or (VAL f) . p = 1 ) by XBOOLEAN:def 3;
A2: ( (VAL f) . q = 0 or (VAL f) . q = 1 ) by XBOOLEAN:def 3;
thus (VAL f) . ((p => q) => (('not' q) => ('not' p))) = ((VAL f) . (p => q)) => ((VAL f) . (('not' q) => ('not' p))) by Def15
.= (((VAL f) . p) => ((VAL f) . q)) => ((VAL f) . (('not' q) => ('not' p))) by Def15
.= (((VAL f) . p) => ((VAL f) . q)) => (((VAL f) . (q => TFALSUM)) => ((VAL f) . (p => TFALSUM))) by Def15
.= (((VAL f) . p) => ((VAL f) . q)) => ((((VAL f) . q) => ((VAL f) . TFALSUM)) => ((VAL f) . (p => TFALSUM))) by Def15
.= (((VAL f) . p) => ((VAL f) . q)) => ((((VAL f) . q) => FALSE) => ((VAL f) . (p => TFALSUM))) by Def15
.= (((VAL f) . p) => ((VAL f) . q)) => ((((VAL f) . q) => FALSE) => (((VAL f) . p) => ((VAL f) . TFALSUM))) by Def15
.= 1 by A1, A2 ; :: thesis: verum

end;

then (p => q) => (('not' q) => ('not' p)) is LTL_TAUT_OF_PL ;
then (p => q) => (('not' q) => ('not' p)) in LTL_axioms by Def17;
then A3: X |- (p => q) => (('not' q) => ('not' p)) by Th42;
assume X |- p => q ; :: thesis: X |- ('not' q) => ('not' p)
hence X |- ('not' q) => ('not' p) by A3, Th43; :: thesis: verum