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

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