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