let X, A be set ; :: thesis: ( X in A implies X c= union A )
assume A1: X in A ; :: thesis: X c= union A
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in X or x in union A )
thus ( not x in X or x in union A ) by A1, TARSKI:def 4; :: thesis: verum