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

for O1, O2 being Operation of X

for n, m being Nat st n <= m & L1 c= L2 & O1 c= O2 holds

L1 WHEREle (O2,n) c= L2 WHEREle (O1,m)

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

for n, m being Nat st n <= m & L1 c= L2 & O1 c= O2 holds

L1 WHEREle (O2,n) c= L2 WHEREle (O1,m)

let O1, O2 be Operation of X; :: thesis: for n, m being Nat st n <= m & L1 c= L2 & O1 c= O2 holds

L1 WHEREle (O2,n) c= L2 WHEREle (O1,m)

let n, m be Nat; :: thesis: ( n <= m & L1 c= L2 & O1 c= O2 implies L1 WHEREle (O2,n) c= L2 WHEREle (O1,m) )

assume A1: ( n <= m & L1 c= L2 & O1 c= O2 ) ; :: thesis: L1 WHEREle (O2,n) c= L2 WHEREle (O1,m)

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in L1 WHEREle (O2,n) or z in L2 WHEREle (O1,m) )

assume z in L1 WHEREle (O2,n) ; :: thesis: z in L2 WHEREle (O1,m)

then consider x being Element of X such that

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

( Segm n c= Segm m & x . O1 c= x . O2 ) by A1, Th1, NAT_1:39;

then ( card (x . O1) c= card (x . O2) & card (x . O2) c= m ) by A2, CARD_1:11;

then card (x . O1) c= m ;

hence z in L2 WHEREle (O1,m) by A1, A2; :: thesis: verum

for O1, O2 being Operation of X

for n, m being Nat st n <= m & L1 c= L2 & O1 c= O2 holds

L1 WHEREle (O2,n) c= L2 WHEREle (O1,m)

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

for n, m being Nat st n <= m & L1 c= L2 & O1 c= O2 holds

L1 WHEREle (O2,n) c= L2 WHEREle (O1,m)

let O1, O2 be Operation of X; :: thesis: for n, m being Nat st n <= m & L1 c= L2 & O1 c= O2 holds

L1 WHEREle (O2,n) c= L2 WHEREle (O1,m)

let n, m be Nat; :: thesis: ( n <= m & L1 c= L2 & O1 c= O2 implies L1 WHEREle (O2,n) c= L2 WHEREle (O1,m) )

assume A1: ( n <= m & L1 c= L2 & O1 c= O2 ) ; :: thesis: L1 WHEREle (O2,n) c= L2 WHEREle (O1,m)

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in L1 WHEREle (O2,n) or z in L2 WHEREle (O1,m) )

assume z in L1 WHEREle (O2,n) ; :: thesis: z in L2 WHEREle (O1,m)

then consider x being Element of X such that

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

( Segm n c= Segm m & x . O1 c= x . O2 ) by A1, Th1, NAT_1:39;

then ( card (x . O1) c= card (x . O2) & card (x . O2) c= m ) by A2, CARD_1:11;

then card (x . O1) c= m ;

hence z in L2 WHEREle (O1,m) by A1, A2; :: thesis: verum