let p, q be Element of LTLB_WFF ; :: thesis: p => (q => p) in LTL_axioms
p => (q => p) is LTL_TAUT_OF_PL

proof

let f be Function of LTLB_WFF,BOOLEAN; :: according to LTLAXIO1:def 16 :: thesis: (VAL f) . (p => (q => p)) = 1
A1: ( (VAL f) . p = 0 or (VAL f) . p = 1 ) by XBOOLEAN:def 3;
thus (VAL f) . (p => (q => p)) = ((VAL f) . p) => ((VAL f) . (q => p)) by Def15
.= ((VAL f) . p) => (((VAL f) . q) => ((VAL f) . p)) by Def15
.= 1 by A1 ; :: thesis: verum

end;

hence p => (q => p) in LTL_axioms by Def17; :: thesis: verum