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