theorem :: ROUGHS_3:48

for R1, R2, R being non empty RelStr
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