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

LAp X = (LAp X1) /\ (LAp 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

LAp X = (LAp X1) /\ (LAp 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

LAp X = (LAp X1) /\ (LAp 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 LAp X = (LAp X1) /\ (LAp X2) )

assume A1: ( R = Union (R1,R2) & X = X1 & X = X2 & the carrier of R1 = the carrier of R2 ) ; :: thesis: LAp X = (LAp X1) /\ (LAp 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;

D1: LAp X c= (LAp X1) /\ (LAp 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

LAp X = (LAp X1) /\ (LAp 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

LAp X = (LAp X1) /\ (LAp 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

LAp X = (LAp X1) /\ (LAp 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 LAp X = (LAp X1) /\ (LAp X2) )

assume A1: ( R = Union (R1,R2) & X = X1 & X = X2 & the carrier of R1 = the carrier of R2 ) ; :: thesis: LAp X = (LAp X1) /\ (LAp 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;

D1: LAp X c= (LAp X1) /\ (LAp X2)

proof

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

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

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

then consider xx being Element of R such that

E1: ( xx = x & Class ( the InternalRel of R,xx) c= X ) ;

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

Class ( the InternalRel of R1,x1) c= X1

then T1: x1 in LAp X1 by ROUGHS_1:def 4;

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

Class ( the InternalRel of R2,x2) c= X2

then x2 in LAp X2 by ROUGHS_1:def 4;

hence x in (LAp X1) /\ (LAp X2) by T1, E1, XBOOLE_0:def 4; :: thesis: verum

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

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

then consider xx being Element of R such that

E1: ( xx = x & Class ( the InternalRel of R,xx) c= X ) ;

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

Class ( the InternalRel of R1,x1) c= X1

proof

then
x1 in { x where x is Element of R1 : Class ( the InternalRel of R1,x) c= X1 }
;
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in Class ( the InternalRel of R1,x1) or y in X1 )

assume F1: y in Class ( the InternalRel of R1,x1) ; :: thesis: y in X1

then reconsider y1 = y as Element of R1 ;

[x1,y1] in the InternalRel of R1 by F1, RELAT_1:169;

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

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

hence y in X1 by E1, A1; :: thesis: verum

end;assume F1: y in Class ( the InternalRel of R1,x1) ; :: thesis: y in X1

then reconsider y1 = y as Element of R1 ;

[x1,y1] in the InternalRel of R1 by F1, RELAT_1:169;

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

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

hence y in X1 by E1, A1; :: thesis: verum

then T1: x1 in LAp X1 by ROUGHS_1:def 4;

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

Class ( the InternalRel of R2,x2) c= X2

proof

then
x2 in { x where x is Element of R2 : Class ( the InternalRel of R2,x) c= X2 }
;
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in Class ( the InternalRel of R2,x2) or y in X2 )

assume F1: y in Class ( the InternalRel of R2,x2) ; :: thesis: y in X2

then reconsider y2 = y as Element of R2 ;

[x2,y2] in the InternalRel of R2 by F1, RELAT_1:169;

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

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

hence y in X2 by E1, A1; :: thesis: verum

end;assume F1: y in Class ( the InternalRel of R2,x2) ; :: thesis: y in X2

then reconsider y2 = y as Element of R2 ;

[x2,y2] in the InternalRel of R2 by F1, RELAT_1:169;

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

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

hence y in X2 by E1, A1; :: thesis: verum

then x2 in LAp X2 by ROUGHS_1:def 4;

hence x in (LAp X1) /\ (LAp X2) by T1, E1, XBOOLE_0:def 4; :: thesis: verum

proof

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

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

then H0: ( x in LAp X1 & x in LAp X2 ) by XBOOLE_0:def 4;

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

then consider x1 being Element of R1 such that

H1: ( x1 = x & Class ( the InternalRel of R1,x1) c= X1 ) ;

x in { x where x is Element of R2 : Class ( the InternalRel of R2,x) c= X2 } by H0, ROUGHS_1:def 4;

then consider x2 being Element of R2 such that

H2: ( x2 = x & Class ( the InternalRel of R2,x2) c= X2 ) ;

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

Class ( the InternalRel of R,xx) c= X

hence x in LAp X by ROUGHS_1:def 4; :: thesis: verum

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

then H0: ( x in LAp X1 & x in LAp X2 ) by XBOOLE_0:def 4;

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

then consider x1 being Element of R1 such that

H1: ( x1 = x & Class ( the InternalRel of R1,x1) c= X1 ) ;

x in { x where x is Element of R2 : Class ( the InternalRel of R2,x) c= X2 } by H0, ROUGHS_1:def 4;

then consider x2 being Element of R2 such that

H2: ( x2 = x & Class ( the InternalRel of R2,x2) c= X2 ) ;

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

Class ( the InternalRel of R,xx) c= X

proof

then
xx in { x where x is Element of R : Class ( the InternalRel of R,x) c= X }
;
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in Class ( the InternalRel of R,xx) or y in X )

assume S1: y in Class ( the InternalRel of R,xx) ; :: thesis: y in X

then reconsider yy = y as Element of R ;

[xx,yy] in the InternalRel of R by S1, RELAT_1:169;

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

then ( yy in Class ( the InternalRel of R1,xx) or yy in Class ( the InternalRel of R2,xx) ) by RELAT_1:169;

hence y in X by A1, H2, H1; :: thesis: verum

end;assume S1: y in Class ( the InternalRel of R,xx) ; :: thesis: y in X

then reconsider yy = y as Element of R ;

[xx,yy] in the InternalRel of R by S1, RELAT_1:169;

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

then ( yy in Class ( the InternalRel of R1,xx) or yy in Class ( the InternalRel of R2,xx) ) by RELAT_1:169;

hence y in X by A1, H2, H1; :: thesis: verum

hence x in LAp X by ROUGHS_1:def 4; :: thesis: verum