let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in ROUGH (A,1) or z in Union A )
assume z in ROUGH (A,1) ; :: thesis: z in Union A
then z in { x where x is Element of X : 1 <= #occurrences (x,A) } by Def24;
then consider x being Element of X such that
A1: ( z = x & 1 <= #occurrences (x,A) ) ;
1 = 0 + 1 ;
then #occurrences (x,A) > 0 by A1, NAT_1:13;
then { i where i is Element of NAT : ( i in dom A & x in A . i ) } <> {} ;
then consider s being object such that
A2: s in { i where i is Element of NAT : ( i in dom A & x in A . i ) } by XBOOLE_0:def 1;
consider i being Element of NAT such that
A3: ( s = i & i in dom A & x in A . i ) by A2;
thus z in Union A by A1, A3, CARD_5:2; :: thesis: verum