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))

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

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 O or z in L WHERE (NOT (NOT O)) )
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;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

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