let R1, R2, R be non empty RelStr ; 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; 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; 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; ( 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 )
; 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
let x be
object ;
TARSKI:def 3 ( not x in UAp X or x in (UAp X1) \/ (UAp X2) )
assume
x in UAp X
;
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;
verum
end;
(UAp X1) \/ (UAp X2) c= UAp X
proof
let x be
object ;
TARSKI:def 3 ( not x in (UAp X1) \/ (UAp X2) or x in UAp X )
assume
x in (UAp X1) \/ (UAp X2)
;
x in UAp X
per cases then
( x in UAp X1 or x in UAp X2 )
by XBOOLE_0:def 3;
suppose
x in UAp X1
;
x in UAp Xthen
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;
verum end; suppose
x in UAp X2
;
x in UAp Xthen
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;
verum end;
end;
hence
UAp X = (UAp X1) \/ (UAp X2)
by XBOOLE_0:def 10, C1; verum