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