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)

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

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