let p be Element of LTLB_WFF ; :: thesis: for X being Subset of LTLB_WFF st p in tau X holds
tau1 . p c= tau X
let X be Subset of LTLB_WFF; :: thesis: ( p in tau X implies tau1 . p c= tau X )
assume p in tau X ; :: thesis: tau1 . p c= tau X
then consider B being Element of LTLB_WFF such that
A1: B in X and
A2: p in tau1 . B by Def5;
A3: tau1 . B c= tau X by Def5, A1;
tau1 . p c= tau1 . B by A2, Th8;
hence tau1 . p c= tau X by A3; :: thesis: verum