let R1, R2, R be non empty RelStr ; :: thesis: for X being Subset of R

for X1 being Subset of R1

for X2 being Subset of R2 st R = Union (R1,R2) & X = X1 & X = X2 & the carrier of R1 = the carrier of R2 holds

UAp X = (UAp X1) \/ (UAp X2)

let X be Subset of R; :: thesis: for X1 being Subset of R1

for X2 being Subset of R2 st R = Union (R1,R2) & X = X1 & X = X2 & the carrier of R1 = the carrier of R2 holds

UAp X = (UAp X1) \/ (UAp X2)

let X1 be Subset of R1; :: thesis: for X2 being Subset of R2 st R = Union (R1,R2) & X = X1 & X = X2 & the carrier of R1 = the carrier of R2 holds

UAp X = (UAp X1) \/ (UAp X2)

let X2 be Subset of R2; :: thesis: ( R = Union (R1,R2) & X = X1 & X = X2 & the carrier of R1 = the carrier of R2 implies UAp X = (UAp X1) \/ (UAp X2) )

assume A1: ( R = Union (R1,R2) & X = X1 & X = X2 & the carrier of R1 = the carrier of R2 ) ; :: thesis: UAp X = (UAp X1) \/ (UAp X2)

then A0: the InternalRel of R = the InternalRel of R1 \/ the InternalRel of R2 by DefUnion;

b1: the carrier of R = the carrier of R1 \/ the carrier of R2 by A1, DefUnion;

C1: UAp X c= (UAp X1) \/ (UAp X2)

for X1 being Subset of R1

for X2 being Subset of R2 st R = Union (R1,R2) & X = X1 & X = X2 & the carrier of R1 = the carrier of R2 holds

UAp X = (UAp X1) \/ (UAp X2)

let X be Subset of R; :: thesis: for X1 being Subset of R1

for X2 being Subset of R2 st R = Union (R1,R2) & X = X1 & X = X2 & the carrier of R1 = the carrier of R2 holds

UAp X = (UAp X1) \/ (UAp X2)

let X1 be Subset of R1; :: thesis: for X2 being Subset of R2 st R = Union (R1,R2) & X = X1 & X = X2 & the carrier of R1 = the carrier of R2 holds

UAp X = (UAp X1) \/ (UAp X2)

let X2 be Subset of R2; :: thesis: ( R = Union (R1,R2) & X = X1 & X = X2 & the carrier of R1 = the carrier of R2 implies UAp X = (UAp X1) \/ (UAp X2) )

assume A1: ( R = Union (R1,R2) & X = X1 & X = X2 & the carrier of R1 = the carrier of R2 ) ; :: thesis: UAp X = (UAp X1) \/ (UAp X2)

then A0: the InternalRel of R = the InternalRel of R1 \/ the InternalRel of R2 by DefUnion;

b1: the carrier of R = the carrier of R1 \/ the carrier of R2 by A1, DefUnion;

C1: UAp X c= (UAp X1) \/ (UAp X2)

proof

(UAp X1) \/ (UAp X2) c= UAp X
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in UAp X or x in (UAp X1) \/ (UAp X2) )

assume x in UAp X ; :: thesis: x in (UAp X1) \/ (UAp X2)

then x in { x where x is Element of R : Class ( the InternalRel of R,x) meets X } by ROUGHS_1:def 5;

then consider xx being Element of R such that

A2: ( xx = x & Class ( the InternalRel of R,xx) meets X ) ;

consider z being object such that

A3: ( z in Class ( the InternalRel of R,xx) & z in X ) by A2, XBOOLE_0:3;

reconsider zz = z as Element of R by A3;

[xx,zz] in the InternalRel of R by A3, RELAT_1:169;

then B2: ( [xx,zz] in the InternalRel of R1 or [xx,zz] in the InternalRel of R2 ) by XBOOLE_0:def 3, A0;

reconsider x1 = xx, z1 = zz as Element of R1 by A1, b1;

reconsider x2 = xx, z2 = zz as Element of R2 by A1, b1;

( z1 in Class ( the InternalRel of R1,x1) or z2 in Class ( the InternalRel of R2,x2) ) by B2, RELAT_1:169;

then ( Class ( the InternalRel of R1,x1) meets X or Class ( the InternalRel of R2,x2) meets X ) by A3, XBOOLE_0:3;

then ( x1 in { x where x is Element of R1 : Class ( the InternalRel of R1,x) meets X1 } or x2 in { x where x is Element of R2 : Class ( the InternalRel of R2,x) meets X2 } ) by A1;

then ( x1 in UAp X1 or x2 in UAp X2 ) by ROUGHS_1:def 5;

hence x in (UAp X1) \/ (UAp X2) by A2, XBOOLE_0:def 3; :: thesis: verum

end;assume x in UAp X ; :: thesis: x in (UAp X1) \/ (UAp X2)

then x in { x where x is Element of R : Class ( the InternalRel of R,x) meets X } by ROUGHS_1:def 5;

then consider xx being Element of R such that

A2: ( xx = x & Class ( the InternalRel of R,xx) meets X ) ;

consider z being object such that

A3: ( z in Class ( the InternalRel of R,xx) & z in X ) by A2, XBOOLE_0:3;

reconsider zz = z as Element of R by A3;

[xx,zz] in the InternalRel of R by A3, RELAT_1:169;

then B2: ( [xx,zz] in the InternalRel of R1 or [xx,zz] in the InternalRel of R2 ) by XBOOLE_0:def 3, A0;

reconsider x1 = xx, z1 = zz as Element of R1 by A1, b1;

reconsider x2 = xx, z2 = zz as Element of R2 by A1, b1;

( z1 in Class ( the InternalRel of R1,x1) or z2 in Class ( the InternalRel of R2,x2) ) by B2, RELAT_1:169;

then ( Class ( the InternalRel of R1,x1) meets X or Class ( the InternalRel of R2,x2) meets X ) by A3, XBOOLE_0:3;

then ( x1 in { x where x is Element of R1 : Class ( the InternalRel of R1,x) meets X1 } or x2 in { x where x is Element of R2 : Class ( the InternalRel of R2,x) meets X2 } ) by A1;

then ( x1 in UAp X1 or x2 in UAp X2 ) by ROUGHS_1:def 5;

hence x in (UAp X1) \/ (UAp X2) by A2, XBOOLE_0:def 3; :: thesis: verum

proof

hence
UAp X = (UAp X1) \/ (UAp X2)
by XBOOLE_0:def 10, C1; :: thesis: verum
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (UAp X1) \/ (UAp X2) or x in UAp X )

assume x in (UAp X1) \/ (UAp X2) ; :: thesis: x in UAp X

end;assume x in (UAp X1) \/ (UAp X2) ; :: thesis: x in UAp X

per cases then
( x in UAp X1 or x in UAp X2 )
by XBOOLE_0:def 3;

end;

suppose
x in UAp X1
; :: thesis: x in UAp X

then
x in { x where x is Element of R1 : Class ( the InternalRel of R1,x) meets X1 }
by ROUGHS_1:def 5;

then consider xx being Element of R1 such that

C1: ( xx = x & Class ( the InternalRel of R1,xx) meets X1 ) ;

reconsider xxx = xx as Element of R by A1, b1;

consider z being object such that

C2: ( z in Class ( the InternalRel of R1,xx) & z in X1 ) by C1, XBOOLE_0:3;

reconsider zz = z as Element of R1 by C2;

[xx,zz] in the InternalRel of R1 by C2, RELAT_1:169;

then [xx,zz] in the InternalRel of R1 \/ the InternalRel of R2 by XBOOLE_0:def 3;

then zz in Class ( the InternalRel of R,xx) by A0, RELAT_1:169;

then Class ( the InternalRel of R,xx) meets X1 by C2, XBOOLE_0:3;

then xxx in { x where x is Element of R : Class ( the InternalRel of R,x) meets X } by A1;

hence x in UAp X by C1, ROUGHS_1:def 5; :: thesis: verum

end;then consider xx being Element of R1 such that

C1: ( xx = x & Class ( the InternalRel of R1,xx) meets X1 ) ;

reconsider xxx = xx as Element of R by A1, b1;

consider z being object such that

C2: ( z in Class ( the InternalRel of R1,xx) & z in X1 ) by C1, XBOOLE_0:3;

reconsider zz = z as Element of R1 by C2;

[xx,zz] in the InternalRel of R1 by C2, RELAT_1:169;

then [xx,zz] in the InternalRel of R1 \/ the InternalRel of R2 by XBOOLE_0:def 3;

then zz in Class ( the InternalRel of R,xx) by A0, RELAT_1:169;

then Class ( the InternalRel of R,xx) meets X1 by C2, XBOOLE_0:3;

then xxx in { x where x is Element of R : Class ( the InternalRel of R,x) meets X } by A1;

hence x in UAp X by C1, ROUGHS_1:def 5; :: thesis: verum

suppose
x in UAp X2
; :: thesis: x in UAp X

then
x in { x where x is Element of R2 : Class ( the InternalRel of R2,x) meets X2 }
by ROUGHS_1:def 5;

then consider xx being Element of R2 such that

C1: ( xx = x & Class ( the InternalRel of R2,xx) meets X2 ) ;

reconsider xxx = xx as Element of R by b1, A1;

consider z being object such that

C2: ( z in Class ( the InternalRel of R2,xx) & z in X2 ) by C1, XBOOLE_0:3;

reconsider zz = z as Element of R2 by C2;

[xx,zz] in the InternalRel of R2 by C2, RELAT_1:169;

then [xx,zz] in the InternalRel of R1 \/ the InternalRel of R2 by XBOOLE_0:def 3;

then zz in Class ( the InternalRel of R,xx) by A0, RELAT_1:169;

then Class ( the InternalRel of R,xx) meets X2 by C2, XBOOLE_0:3;

then xxx in { x where x is Element of R : Class ( the InternalRel of R,x) meets X } by A1;

hence x in UAp X by C1, ROUGHS_1:def 5; :: thesis: verum

end;then consider xx being Element of R2 such that

C1: ( xx = x & Class ( the InternalRel of R2,xx) meets X2 ) ;

reconsider xxx = xx as Element of R by b1, A1;

consider z being object such that

C2: ( z in Class ( the InternalRel of R2,xx) & z in X2 ) by C1, XBOOLE_0:3;

reconsider zz = z as Element of R2 by C2;

[xx,zz] in the InternalRel of R2 by C2, RELAT_1:169;

then [xx,zz] in the InternalRel of R1 \/ the InternalRel of R2 by XBOOLE_0:def 3;

then zz in Class ( the InternalRel of R,xx) by A0, RELAT_1:169;

then Class ( the InternalRel of R,xx) meets X2 by C2, XBOOLE_0:3;

then xxx in { x where x is Element of R : Class ( the InternalRel of R,x) meets X } by A1;

hence x in UAp X by C1, ROUGHS_1:def 5; :: thesis: verum