let K be Relation; :: thesis: ( rng K is empty-membered implies union (rng K) = {} )
assume A2: rng K is empty-membered ; :: thesis: union (rng K) = {}
now :: thesis: for x being object st x in union (rng K) holds
x in {}
let x be object ; :: thesis: ( x in union (rng K) implies x in {} )
assume x in union (rng K) ; :: thesis: x in {}
then ex A being set st
( x in A & A in rng K ) by TARSKI:def 4;
hence x in {} by A2; :: thesis: verum
end;
then union (rng K) c= {} by TARSKI:def 3;
hence union (rng K) = {} ; :: thesis: verum