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)
proof
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
proof
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;
then x1 in { x where x is Element of R1 : Class ( the InternalRel of R1,x) 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
proof
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;
then x2 in { x where x is Element of R2 : Class ( the InternalRel of R2,x) 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;
(LAp X1) /\ (LAp X2) c= LAp X
proof
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
proof
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;
then xx in { x where x is Element of R : Class ( the InternalRel of R,x) c= X } ;
hence x in LAp X by ROUGHS_1:def 4; :: thesis: verum
end;
hence LAp X = (LAp X1) /\ (LAp X2) by D1, XBOOLE_0:def 10; :: thesis: verum