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
UAp X c= (UAp X1) /\ (UAp X2)
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
UAp X c= (UAp X1) /\ (UAp X2)
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
UAp X c= (UAp X1) /\ (UAp X2)
let X2 be Subset of R2; :: thesis: ( R = Meet (R1,R2) & X = X1 & X = X2 & the carrier of R1 = the carrier of R2 implies UAp X c= (UAp X1) /\ (UAp X2) )
assume A1: ( R = Meet (R1,R2) & X = X1 & X = X2 & the carrier of R1 = the carrier of R2 ) ; :: thesis: UAp X c= (UAp X1) /\ (UAp X2)
SS: the InternalRel of R = the InternalRel of R1 /\ the InternalRel of R2 by A1, DefMeet;
sz: 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 ;
zz: dom (UAp R) = bool the carrier of R by FUNCT_2:def 1;
UAp X c= (UAp X1) /\ (UAp X2)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in UAp X or x in (UAp X1) /\ (UAp X2) )
assume S2: x in UAp X ; :: thesis: x in (UAp X1) /\ (UAp X2)
UAp R cc= UAp R1 by Prop16H, SS, sz, A1, XBOOLE_1:17;
then (UAp R) . XX c= (UAp R1) . XX1 by zz, ALTCAT_2:def 1;
then (UAp R) . XX c= UAp XX1 by ROUGHS_2:def 11;
then hh: UAp XX c= UAp XX1 by ROUGHS_2:def 11;
UAp R cc= UAp R2 by Prop16H, A1, SS, XBOOLE_1:17, sz;
then (UAp R) . XX c= (UAp R2) . XX2 by zz, ALTCAT_2:def 1;
then (UAp R) . XX c= UAp XX2 by ROUGHS_2:def 11;
then UAp XX c= UAp XX2 by ROUGHS_2:def 11;
hence x in (UAp X1) /\ (UAp X2) by hh, XBOOLE_0:def 4, S2, A1; :: thesis: verum

end;

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