let X be set ; 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 WHEREge (O1,m) c= L2 WHEREge (O2,n)
let L1, L2 be 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 WHEREge (O1,m) c= L2 WHEREge (O2,n)
let O1, O2 be Operation of X; for n, m being Nat st n <= m & L1 c= L2 & O1 c= O2 holds
L1 WHEREge (O1,m) c= L2 WHEREge (O2,n)
let n, m be Nat; ( n <= m & L1 c= L2 & O1 c= O2 implies L1 WHEREge (O1,m) c= L2 WHEREge (O2,n) )
assume A1:
( n <= m & L1 c= L2 & O1 c= O2 )
; L1 WHEREge (O1,m) c= L2 WHEREge (O2,n)
let z be object ; TARSKI:def 3 ( not z in L1 WHEREge (O1,m) or z in L2 WHEREge (O2,n) )
assume
z in L1 WHEREge (O1,m)
; z in L2 WHEREge (O2,n)
then consider x being Element of X such that
A2:
( z = x & m c= card (x . O1) & x in L1 )
;
( Segm n c= Segm m & x . O1 c= x . O2 )
by A1, Th1, NAT_1:39;
then
( n c= card (x . O1) & card (x . O1) c= card (x . O2) )
by A2, CARD_1:11;
then
n c= card (x . O2)
;
hence
z in L2 WHEREge (O2,n)
by A1, A2; verum