let R1, R2, R be non empty RelStr ; :: thesis:
let X be Subset of R; :: thesis:
let X1 be Subset of R1; :: thesis:
let X2 be Subset of R2; :: thesis:
assume A1: ( R = Meet (R1,R2) & X = X1 & X = X2 & the carrier of R1 = the carrier of R2 ) ; :: thesis:
SS: the InternalRel of R = the InternalRel of R1 /\ the InternalRel of R2 by A1, DefMeet;
sa: dom (LAp R1) = bool the carrier of R1 by FUNCT_2:def 1;
sw: dom (LAp R2) = bool the carrier of R2 by FUNCT_2:def 1;
aa: the carrier of R = the carrier of R1 /\ the carrier of R2 by A1, DefMeet;
reconsider XX1 = X as Subset of R1 by A1;
reconsider XX2 = X as Subset of R2 by A1;
reconsider XX = X as Subset of R ;
(LAp X1) \/ (LAp X2) c= LAp X

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in (LAp X1) \/ (LAp X2) ; :: thesis:

per cases by XBOOLE_0:def 3;

suppose S2: x in LAp X1 ; :: thesis:

LAp R1 cc= LAp R by aa, A1, Prop16L, SS, XBOOLE_1:17;
then (LAp R1) . XX1 c= (LAp R) . XX by sa, ALTCAT_2:def 1;
then (LAp R1) . XX1 c= LAp XX by ROUGHS_2:def 10;
then LAp XX1 c= LAp XX by ROUGHS_2:def 10;
hence x in LAp X by S2, A1; :: thesis:

end;

suppose S2: x in LAp X2 ; :: thesis:

LAp R2 cc= LAp R by aa, Prop16L, A1, SS, XBOOLE_1:17;
then (LAp R2) . XX2 c= (LAp R) . XX by sw, ALTCAT_2:def 1;
then (LAp R2) . XX2 c= LAp XX by ROUGHS_2:def 10;
then LAp XX2 c= LAp XX by ROUGHS_2:def 10;
hence x in LAp X by S2, A1; :: thesis:

end;

end;

end;

hence (LAp X1) \/ (LAp X2) c= LAp X ; :: thesis: