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

for O, O1, O2, O3 being Operation of X st O1 c= O2 & L1 c= L2 & O c= O3 holds

L1 WHEREle (O3,O1) c= L2 WHEREle (O,O2)

let L1, L2 be List of X; :: thesis: for O, O1, O2, O3 being Operation of X st O1 c= O2 & L1 c= L2 & O c= O3 holds

L1 WHEREle (O3,O1) c= L2 WHEREle (O,O2)

let O, O1, O2, O3 be Operation of X; :: thesis: ( O1 c= O2 & L1 c= L2 & O c= O3 implies L1 WHEREle (O3,O1) c= L2 WHEREle (O,O2) )

assume A1: ( O1 c= O2 & L1 c= L2 & O c= O3 ) ; :: thesis: L1 WHEREle (O3,O1) c= L2 WHEREle (O,O2)

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

assume z in L1 WHEREle (O3,O1) ; :: thesis: z in L2 WHEREle (O,O2)

then consider x being Element of X such that

A2: ( z = x & card (x . O3) c= card (x . O1) & x in L1 ) ;

A3: ( card (x . O1) c= card (x . O2) & card (x . O) c= card (x . O3) ) by A1, Th1, CARD_1:11;

then card (x . O3) c= card (x . O2) by A2;

then card (x . O) c= card (x . O2) by A3;

hence z in L2 WHEREle (O,O2) by A2, A1; :: thesis: verum

for O, O1, O2, O3 being Operation of X st O1 c= O2 & L1 c= L2 & O c= O3 holds

L1 WHEREle (O3,O1) c= L2 WHEREle (O,O2)

let L1, L2 be List of X; :: thesis: for O, O1, O2, O3 being Operation of X st O1 c= O2 & L1 c= L2 & O c= O3 holds

L1 WHEREle (O3,O1) c= L2 WHEREle (O,O2)

let O, O1, O2, O3 be Operation of X; :: thesis: ( O1 c= O2 & L1 c= L2 & O c= O3 implies L1 WHEREle (O3,O1) c= L2 WHEREle (O,O2) )

assume A1: ( O1 c= O2 & L1 c= L2 & O c= O3 ) ; :: thesis: L1 WHEREle (O3,O1) c= L2 WHEREle (O,O2)

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

assume z in L1 WHEREle (O3,O1) ; :: thesis: z in L2 WHEREle (O,O2)

then consider x being Element of X such that

A2: ( z = x & card (x . O3) c= card (x . O1) & x in L1 ) ;

A3: ( card (x . O1) c= card (x . O2) & card (x . O) c= card (x . O3) ) by A1, Th1, CARD_1:11;

then card (x . O3) c= card (x . O2) by A2;

then card (x . O) c= card (x . O2) by A3;

hence z in L2 WHEREle (O,O2) by A2, A1; :: thesis: verum