assume
not tau X is empty
; :: thesis: contradiction

then consider x being object such that

A1: x in tau X ;

ex p being Element of LTLB_WFF st

( p in X & x in tau1 . p ) by A1, Def5;

hence contradiction ; :: thesis: verum

then consider x being object such that

A1: x in tau X ;

ex p being Element of LTLB_WFF st

( p in X & x in tau1 . p ) by A1, Def5;

hence contradiction ; :: thesis: verum