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

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

L1 WHERE O1 c= L2 WHERE O2

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

L1 WHERE O1 c= L2 WHERE O2

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

assume A1: ( O1 c= O2 & L1 c= L2 ) ; :: thesis: L1 WHERE O1 c= L2 WHERE O2

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

assume A2: z in L1 WHERE O1 ; :: thesis: z in L2 WHERE O2

then reconsider z = z as Element of X ;

A3: ( z . O1 <> {} & z in L1 ) by A2, Th3;

z . O1 c= z . O2 by A1, Th1;

then z . O2 <> {} by A3;

hence z in L2 WHERE O2 by A1, A3, Th3; :: thesis: verum

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

L1 WHERE O1 c= L2 WHERE O2

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

L1 WHERE O1 c= L2 WHERE O2

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

assume A1: ( O1 c= O2 & L1 c= L2 ) ; :: thesis: L1 WHERE O1 c= L2 WHERE O2

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

assume A2: z in L1 WHERE O1 ; :: thesis: z in L2 WHERE O2

then reconsider z = z as Element of X ;

A3: ( z . O1 <> {} & z in L1 ) by A2, Th3;

z . O1 c= z . O2 by A1, Th1;

then z . O2 <> {} by A3;

hence z in L2 WHERE O2 by A1, A3, Th3; :: thesis: verum