let X be set ; :: thesis: for L1, L2 being List of X

for O being Operation of X

for n being Nat st n <> 0 & L1 c= L2 holds

L1 WHEREeq (O,n) c= L2 WHERE O

let L1, L2 be List of X; :: thesis: for O being Operation of X

for n being Nat st n <> 0 & L1 c= L2 holds

L1 WHEREeq (O,n) c= L2 WHERE O

let O be Operation of X; :: thesis: for n being Nat st n <> 0 & L1 c= L2 holds

L1 WHEREeq (O,n) c= L2 WHERE O

let n be Nat; :: thesis: ( n <> 0 & L1 c= L2 implies L1 WHEREeq (O,n) c= L2 WHERE O )

assume A1: ( n <> 0 & L1 c= L2 ) ; :: thesis: L1 WHEREeq (O,n) c= L2 WHERE O

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in L1 WHEREeq (O,n) or z in L2 WHERE O )

assume z in L1 WHEREeq (O,n) ; :: thesis: z in L2 WHERE O

then consider x being Element of X such that

A2: ( z = x & card (x . O) = n & x in L1 ) ;

x . O <> {} by A1, A2;

hence z in L2 WHERE O by A1, A2, Th3; :: thesis: verum

for O being Operation of X

for n being Nat st n <> 0 & L1 c= L2 holds

L1 WHEREeq (O,n) c= L2 WHERE O

let L1, L2 be List of X; :: thesis: for O being Operation of X

for n being Nat st n <> 0 & L1 c= L2 holds

L1 WHEREeq (O,n) c= L2 WHERE O

let O be Operation of X; :: thesis: for n being Nat st n <> 0 & L1 c= L2 holds

L1 WHEREeq (O,n) c= L2 WHERE O

let n be Nat; :: thesis: ( n <> 0 & L1 c= L2 implies L1 WHEREeq (O,n) c= L2 WHERE O )

assume A1: ( n <> 0 & L1 c= L2 ) ; :: thesis: L1 WHEREeq (O,n) c= L2 WHERE O

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in L1 WHEREeq (O,n) or z in L2 WHERE O )

assume z in L1 WHEREeq (O,n) ; :: thesis: z in L2 WHERE O

then consider x being Element of X such that

A2: ( z = x & card (x . O) = n & x in L1 ) ;

x . O <> {} by A1, A2;

hence z in L2 WHERE O by A1, A2, Th3; :: thesis: verum