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

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