let X be set ; :: thesis: for L being List of X

for O being Operation of X st L c= dom O holds

L WHERE O = L

let L be List of X; :: thesis: for O being Operation of X st L c= dom O holds

L WHERE O = L

let O be Operation of X; :: thesis: ( L c= dom O implies L WHERE O = L )

assume A1: L c= dom O ; :: thesis: L WHERE O = L

thus L WHERE O c= L by Th4; :: according to XBOOLE_0:def 10 :: thesis: L c= L WHERE O

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in L or z in L WHERE O )

assume A2: z in L ; :: thesis: z in L WHERE O

then reconsider z = z as Element of X ;

z . O <> {} by A1, A2, RELAT_1:170;

hence z in L WHERE O by A2, Th3; :: thesis: verum

for O being Operation of X st L c= dom O holds

L WHERE O = L

let L be List of X; :: thesis: for O being Operation of X st L c= dom O holds

L WHERE O = L

let O be Operation of X; :: thesis: ( L c= dom O implies L WHERE O = L )

assume A1: L c= dom O ; :: thesis: L WHERE O = L

thus L WHERE O c= L by Th4; :: according to XBOOLE_0:def 10 :: thesis: L c= L WHERE O

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in L or z in L WHERE O )

assume A2: z in L ; :: thesis: z in L WHERE O

then reconsider z = z as Element of X ;

z . O <> {} by A1, A2, RELAT_1:170;

hence z in L WHERE O by A2, Th3; :: thesis: verum