let X be set ; :: thesis: for L being List of X
for O being Operation of X holds L WHERE (NOT (NOT O)) = L WHERE O
let L be List of X; :: thesis: for O being Operation of X holds L WHERE (NOT (NOT O)) = L WHERE O
let O be Operation of X; :: thesis: L WHERE (NOT (NOT O)) = L WHERE O
thus L WHERE (NOT (NOT O)) c= L WHERE O :: according to XBOOLE_0:def 10 :: thesis: L WHERE O c= L WHERE (NOT (NOT O))

proof

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in L WHERE (NOT (NOT O)) or z in L WHERE O )
assume A1: z in L WHERE (NOT (NOT O)) ; :: thesis: z in L WHERE O
then reconsider x = z as Element of X ;
A2: ( x in L & x . (NOT (NOT O)) <> {} ) by A1, Th3;
then x in dom (NOT (NOT O)) by RELAT_1:170;
then x in dom O by Th38;
then x . O <> {} by RELAT_1:170;
hence z in L WHERE O by A2, Th3; :: thesis: verum

end;

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in L WHERE O or z in L WHERE (NOT (NOT O)) )
assume A3: z in L WHERE O ; :: thesis: z in L WHERE (NOT (NOT O))
then reconsider x = z as Element of X ;
A4: ( z in L & x . O <> {} ) by A3, Th3;
then x in dom O by RELAT_1:170;
then x in dom (NOT (NOT O)) by Th38;
then x . (NOT (NOT O)) <> {} by RELAT_1:170;
hence z in L WHERE (NOT (NOT O)) by A4, Th3; :: thesis: verum