let U0 be with_const_op Universal_Algebra; :: thesis: for U1, U2 being SubAlgebra of U0 holds the carrier of U1 meets the carrier of U2
let U1, U2 be SubAlgebra of U0; :: thesis: the carrier of U1 meets the carrier of U2
consider a being Element of Constants U0;
( Constants U0 is non empty Subset of U1 & Constants U0 is non empty Subset of U2 ) by Th18;
then A1: Constants U0 c= the carrier of U1 /\ the carrier of U2 by XBOOLE_1:19;
a in Constants U0 ;
hence the carrier of U1 meets the carrier of U2 by A1, XBOOLE_0:4; :: thesis: verum