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 = Meet (R1,R2) & X = X1 & X = X2 & the carrier of R1 = the carrier of R2 holds
(LAp X1) \/ (LAp X2) c= LAp X
let X be Subset of R; :: thesis: for X1 being Subset of R1
for X2 being Subset of R2 st R = Meet (R1,R2) & X = X1 & X = X2 & the carrier of R1 = the carrier of R2 holds
(LAp X1) \/ (LAp X2) c= LAp X
let X1 be Subset of R1; :: thesis: for X2 being Subset of R2 st R = Meet (R1,R2) & X = X1 & X = X2 & the carrier of R1 = the carrier of R2 holds
(LAp X1) \/ (LAp X2) c= LAp X
let X2 be Subset of R2; :: thesis: ( R = Meet (R1,R2) & X = X1 & X = X2 & the carrier of R1 = the carrier of R2 implies (LAp X1) \/ (LAp X2) c= LAp X )
assume A1: ( R = Meet (R1,R2) & X = X1 & X = X2 & the carrier of R1 = the carrier of R2 ) ; :: thesis: (LAp X1) \/ (LAp X2) c= LAp X
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: ( not x in (LAp X1) \/ (LAp X2) or x in LAp X )
assume x in (LAp X1) \/ (LAp X2) ; :: thesis: x in LAp X

per cases then ( x in LAp X1 or x in LAp X2 ) by XBOOLE_0:def 3;

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

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: verum

end;

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

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: verum

end;

end;

end;

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