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

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

hence
(LAp X1) \/ (LAp X2) c= LAp X
; :: thesis: verum
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

end;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;

end;