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)
proof
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;
thus tau X c= tau (tau X) by Th16; :: thesis: verum