let X be Subset of LTLB_WFF; :: thesis: ( X is without_implication implies tau X = X )
assume A1: X is without_implication ; :: thesis: tau X = X
A2: tau X c= X

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in tau X or x in X )
assume x in tau X ; :: thesis: x in X
then consider p being Element of LTLB_WFF such that
A3: p in X and
A4: x in tau1 . p by Def5;
x in {p} by A3, A1, Th5, A4;
hence x in X by A3, TARSKI:def 1; :: thesis: verum

end;

X c= tau X by Th16;
hence tau X = X by A2; :: thesis: verum