reconsider A1 = the carrier of X1, A2 = the carrier of X2 as Subset of X by Th1;
set A = A1 \/ A2;
reconsider A = A1 \/ A2 as non empty Subset of X ;
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