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

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

assume A1: X is without_implication ; :: thesis: tau X = X

A2: tau X c= X

proof

X c= tau X
by Th16;
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;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

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