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