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