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
set a = the Element of Constants U0;
( Constants U0 is non empty Subset of U1 & Constants U0 is non empty Subset of U2 ) by Th15;
then A1: Constants U0 c= the carrier of U1 /\ the carrier of U2 by XBOOLE_1:19;
thus the carrier of U1 meets the carrier of U2 by A1; :: thesis: verum