( {(prop 0)} |= 'X' (prop 0) & not {(prop 0)} |=0 'X' (prop 0) ) by th262ac1;
hence ex F being Subset of LTLB_WFF ex A being Element of LTLB_WFF st
( F |= A & not F |=0 A ) ; :: thesis: verum