let X be set ; :: thesis: for L1, L2 being List of X
for O1, O2 being Operation of X st L1 c= L2 & O1 c= O2 holds
L1 | O1 c= L2 | O2
let L1, L2 be List of X; :: thesis: for O1, O2 being Operation of X st L1 c= L2 & O1 c= O2 holds
L1 | O1 c= L2 | O2
let O1, O2 be Operation of X; :: thesis: ( L1 c= L2 & O1 c= O2 implies L1 | O1 c= L2 | O2 )
assume ( L1 c= L2 & O1 c= O2 ) ; :: thesis: L1 | O1 c= L2 | O2
then ( L1 | O1 c= L2 | O1 & L2 | O1 c= L2 | O2 ) by RELAT_1:123, RELAT_1:124;
hence L1 | O1 c= L2 | O2 ; :: thesis: verum