let X be set ; :: thesis: for L1, L2 being List of X
for O being Operation of X st L1 <> {} & L1 c= L2 holds
L2 \& O c= L1 \& O
let L1, L2 be List of X; :: thesis: for O being Operation of X st L1 <> {} & L1 c= L2 holds
L2 \& O c= L1 \& O
let O be Operation of X; :: thesis: ( L1 <> {} & L1 c= L2 implies L2 \& O c= L1 \& O )
assume A1: L1 <> {} ; :: thesis: ( not L1 c= L2 or L2 \& O c= L1 \& O )
assume A2: L1 c= L2 ; :: thesis: L2 \& O c= L1 \& O
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in L2 \& O or z in L1 \& O )
assume A3: z in L2 \& O ; :: thesis: z in L1 \& O

now :: thesis: ( { (x . O) where x is Element of X : x in L1 } <> {} & ( for Y being set st Y in { (x . O) where x is Element of X : x in L1 } holds
z in Y ) )

set c = the Element of L1;
the Element of L1 in L1 by A1;
then reconsider c = the Element of L1 as Element of X ;
c . O in { (x . O) where x is Element of X : x in L1 } by A1;
hence { (x . O) where x is Element of X : x in L1 } <> {} ; :: thesis: for Y being set st Y in { (x . O) where x is Element of X : x in L1 } holds
z in Y
let Y be set ; :: thesis: ( Y in { (x . O) where x is Element of X : x in L1 } implies z in Y )
assume Y in { (x . O) where x is Element of X : x in L1 } ; :: thesis: z in Y
then consider x being Element of X such that
A4: ( Y = x . O & x in L1 ) ;
Y in { (a . O) where a is Element of X : a in L2 } by A4, A2;
hence z in Y by A3, SETFAM_1:def 1; :: thesis: verum

end;

hence z in L1 \& O by SETFAM_1:def 1; :: thesis: verum