A15: for O being Operation of X st O = O2 BUTNOT holds
for L being List of X holds L | O = union { ((x . O1) BUTNOT (x . O2)) where x is Element of X : x in L }

proof

let O be Operation of X; :: thesis: ( O = O2 BUTNOT implies for L being List of X holds L | O = union { ((x . O1) BUTNOT (x . O2)) where x is Element of X : x in L } )
assume A16: O = O1 \ O2 ; :: thesis: for L being List of X holds L | O = union { ((x . O1) BUTNOT (x . O2)) where x is Element of X : x in L }
defpred S₁[ set , set ] means ( [$1,$2] in O1 & not [$1,$2] in O2 );
let L be List of X; :: thesis: L | O = union { ((x . O1) BUTNOT (x . O2)) where x is Element of X : x in L }
thus L | O c= union { ((x . O1) BUTNOT (x . O2)) where x is Element of X : x in L } :: according to XBOOLE_0:def 10 :: thesis: union { ((x . O1) BUTNOT (x . O2)) where x is Element of X : x in L } c= L | O

proof

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in L | O or z in union { ((x . O1) BUTNOT (x . O2)) where x is Element of X : x in L } )
assume z in L | O ; :: thesis: z in union { ((x . O1) BUTNOT (x . O2)) where x is Element of X : x in L }
then consider y being object such that
A17: ( [y,z] in O & y in L ) by RELAT_1:def 13;
reconsider y = y, z = z as Element of X by A17, ZFMISC_1:87;
( [y,z] in O1 & [y,z] nin O2 ) by A16, A17, XBOOLE_0:def 5;
then ( z in y . O1 & z nin y . O2 ) by RELAT_1:169;
then ( z in (y . O1) BUTNOT (y . O2) & (y . O1) BUTNOT (y . O2) in { ((x . O1) BUTNOT (x . O2)) where x is Element of X : x in L } ) by A17, XBOOLE_0:def 5;
hence z in union { ((x . O1) BUTNOT (x . O2)) where x is Element of X : x in L } by TARSKI:def 4; :: thesis: verum

end;

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in union { ((x . O1) BUTNOT (x . O2)) where x is Element of X : x in L } or z in L | O )
assume z in union { ((x . O1) BUTNOT (x . O2)) where x is Element of X : x in L } ; :: thesis: z in L | O
then consider Y being set such that
A18: ( z in Y & Y in { ((x . O1) BUTNOT (x . O2)) where x is Element of X : x in L } ) by TARSKI:def 4;
consider x being Element of X such that
A19: ( Y = (x . O1) BUTNOT (x . O2) & x in L ) by A18;
A20: ( z in x . O1 & not z in x . O2 ) by A18, A19, XBOOLE_0:def 5;
reconsider z = z as Element of X by A18, A19;
( [x,z] in O1 & [x,z] nin O2 ) by A20, RELAT_1:169;
then [x,z] in O by A16, XBOOLE_0:def 5;
hence z in L | O by A19, RELAT_1:def 13; :: thesis: verum

end;

let O be Operation of X; :: thesis: ( O = O2 BUTNOT iff for L being List of X holds L | O = union { ((x . O1) BUTNOT (x . O2)) where x is Element of X : x in L } )
thus ( O = O2 BUTNOT implies for L being List of X holds L | O = union { ((x . O1) BUTNOT (x . O2)) where x is Element of X : x in L } ) by A15; :: thesis: ( ( for L being List of X holds L | O = union { ((x . O1) BUTNOT (x . O2)) where x is Element of X : x in L } ) implies O = O2 BUTNOT )
assume A21: for L being List of X holds L | O = union { ((x . O1) BUTNOT (x . O2)) where x is Element of X : x in L } ; :: thesis: O = O2 BUTNOT

now :: thesis: for L being List of X holds L | O = L | (O1 \ O2)

let L be List of X; :: thesis: L | O = L | (O1 \ O2)
thus L | O = union { ((x . O1) BUTNOT (x . O2)) where x is Element of X : x in L } by A21
.= L | (O1 \ O2) by A15 ; :: thesis: verum

end;

hence O = O2 BUTNOT by Th30; :: thesis: verum