let X be Subset of LTLB_WFF; :: thesis: tau (tau X) = tau X

thus tau (tau X) c= tau X :: according to XBOOLE_0:def 10 :: thesis: tau X c= tau (tau X)

thus tau (tau X) c= tau X :: according to XBOOLE_0:def 10 :: thesis: tau X c= tau (tau X)

proof

thus
tau X c= tau (tau X)
by Th16; :: thesis: verum
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in tau (tau X) or x in tau X )

assume x in tau (tau X) ; :: thesis: x in tau X

then consider p being Element of LTLB_WFF such that

A1: p in tau X and

A2: x in tau1 . p by Def5;

consider q being Element of LTLB_WFF such that

A3: q in X and

A4: p in tau1 . q by A1, Def5;

tau1 . p c= tau1 . q by A4, Th8;

hence x in tau X by A2, A3, Def5; :: thesis: verum

end;assume x in tau (tau X) ; :: thesis: x in tau X

then consider p being Element of LTLB_WFF such that

A1: p in tau X and

A2: x in tau1 . p by Def5;

consider q being Element of LTLB_WFF such that

A3: q in X and

A4: p in tau1 . q by A1, Def5;

tau1 . p c= tau1 . q by A4, Th8;

hence x in tau X by A2, A3, Def5; :: thesis: verum