let X be set ; :: thesis: for L1, L2 being List of X
for O1, O2, O, O3 being Operation of X st O1 c= O2 & L1 c= L2 & O c= O3 holds
L1 WHEREgt (O,O2) c= L2 WHEREgt (O3,O1)
let L1, L2 be List of X; :: thesis: for O1, O2, O, O3 being Operation of X st O1 c= O2 & L1 c= L2 & O c= O3 holds
L1 WHEREgt (O,O2) c= L2 WHEREgt (O3,O1)
let O1, O2, O, O3 be Operation of X; :: thesis: ( O1 c= O2 & L1 c= L2 & O c= O3 implies L1 WHEREgt (O,O2) c= L2 WHEREgt (O3,O1) )
assume Z0: ( O1 c= O2 & L1 c= L2 & O c= O3 ) ; :: thesis: L1 WHEREgt (O,O2) c= L2 WHEREgt (O3,O1)
let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in L1 WHEREgt (O,O2) or z in L2 WHEREgt (O3,O1) )
assume z in L1 WHEREgt (O,O2) ; :: thesis: z in L2 WHEREgt (O3,O1)
then consider x being Element of X such that
A1: ( z = x & card (x . O2) in card (x . O) & x in L1 ) ;
( x . O1 c= x . O2 & x . O c= x . O3 ) by Z0, Th9;
then ( card (x . O1) in card (x . O) & card (x . O) c= card (x . O3) ) by A1, CARD_1:11, ORDINAL1:12;
hence z in L2 WHEREgt (O3,O1) by A1, Z0; :: thesis: verum