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
LAp X = (LAp X1) /\ (LAp 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
LAp X = (LAp X1) /\ (LAp 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
LAp X = (LAp X1) /\ (LAp X2)
let X2 be Subset of R2; ( 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 )
; 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 ;
TARSKI:def 3 ( not x in LAp X or x in (LAp X1) /\ (LAp X2) )
assume
x in LAp X
;
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
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
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;
verum
end;
(LAp X1) /\ (LAp X2) c= LAp X
proof
let x be
object ;
TARSKI:def 3 ( not x in (LAp X1) /\ (LAp X2) or x in LAp X )
assume
x in (LAp X1) /\ (LAp X2)
;
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 ;
TARSKI:def 3 ( not y in Class ( the InternalRel of R,xx) or y in X )
assume S1:
y in Class ( the
InternalRel of
R,
xx)
;
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;
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;
verum
end;
hence
LAp X = (LAp X1) /\ (LAp X2)
by D1, XBOOLE_0:def 10; verum