let M1, M2, M3 be non empty multMagma ; :: thesis: for x3 being Element of M3 holds [3,x3] in FreeAtoms <*M1,M2,M3*>
let x3 be Element of M3; :: thesis: [3,x3] in FreeAtoms <*M1,M2,M3*>
( 3 in {3} & x3 in the carrier of M3 ) by TARSKI:def 1;
then [3,x3] in [:{3}, the carrier of M3:] by ZFMISC_1:def 2;
then [3,x3] in ([:{1}, the carrier of M1:] \/ [:{2}, the carrier of M2:]) \/ [:{3}, the carrier of M3:] by XBOOLE_0:def 3;
hence [3,x3] in FreeAtoms <*M1,M2,M3*> by Th14; :: thesis: verum