reconsider A1 = the carrier of X1, A2 = the carrier of X2 as Subset of X by Th1;
set A = A1 /\ A2;
A1 meets A2 by A1;
then reconsider A = A1 /\ A2 as non empty Subset of X by XBOOLE_0:def 7;
take X | A ; :: thesis: the carrier of (X | A) = the carrier of X1 /\ the carrier of X2
thus the carrier of (X | A) = [#] (X | A)
.= the carrier of X1 /\ the carrier of X2 by PRE_TOPC:def 5 ; :: thesis: verum