let X be set ; :: thesis: for L being List of X
for O being Operation of X holds L WHERE O c= L
let L be List of X; :: thesis: for O being Operation of X holds L WHERE O c= L
let O be Operation of X; :: thesis: L WHERE O c= L
let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in L WHERE O or z in L )
thus ( not z in L WHERE O or z in L ) by ThW; :: thesis: verum