let A be set ; :: thesis: A c= bool (union A)
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in A or x in bool (union A) )
assume x in A ; :: thesis: x in bool (union A)
then x c= union A by Lm15;
hence x in bool (union A) by Def1; :: thesis: verum