defpred S1[ object , object ] means ( Im (O,\$1) = {} & \$2 = \$1 );
consider O1 being Relation such that
A1: for a, b being object holds
( [a,b] in O1 iff ( a in X & b in X & S1[a,b] ) ) from O1 c= [:X,X:]
proof
let x, y be object ; :: according to RELAT_1:def 3 :: thesis: ( not [x,y] in O1 or [x,y] in [:X,X:] )
assume [x,y] in O1 ; :: thesis: [x,y] in [:X,X:]
then ( x in X & y in X ) by A1;
hence [x,y] in [:X,X:] by ZFMISC_1:87; :: thesis: verum
end;
then reconsider O1 = O1 as Operation of X ;
take O1 ; :: thesis: for L being List of X holds L | O1 = union { (IFEQ ((x . O),{},{x},{})) where x is Element of X : x in L }
let L be List of X; :: thesis: L | O1 = union { (IFEQ ((x . O),{},{x},{})) where x is Element of X : x in L }
thus L | O1 c= union { (IFEQ ((x . O),{},{x},{})) where x is Element of X : x in L } :: according to XBOOLE_0:def 10 :: thesis: union { (IFEQ ((x . O),{},{x},{})) where x is Element of X : x in L } c= L | O1
proof
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in L | O1 or a in union { (IFEQ ((x . O),{},{x},{})) where x is Element of X : x in L } )
assume a in L | O1 ; :: thesis: a in union { (IFEQ ((x . O),{},{x},{})) where x is Element of X : x in L }
then consider b being Element of X such that
A2: ( a in b . O1 & b in L ) by Th23;
[b,a] in O1 by ;
then A3: ( a = b & b . O = {} ) by A1;
then B1: a in {b} by TARSKI:def 1;
reconsider Z = IFEQ ((b . O),{},{b},{}) as set ;
A4: a in Z by ;
IFEQ ((b . O),{},{b},{}) in { (IFEQ ((x . O),{},{x},{})) where x is Element of X : x in L } by A2;
hence a in union { (IFEQ ((x . O),{},{x},{})) where x is Element of X : x in L } by ; :: thesis: verum
end;
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in union { (IFEQ ((x . O),{},{x},{})) where x is Element of X : x in L } or a in L | O1 )
assume a in union { (IFEQ ((x . O),{},{x},{})) where x is Element of X : x in L } ; :: thesis: a in L | O1
then consider A being set such that
A5: ( a in A & A in { (IFEQ ((x . O),{},{x},{})) where x is Element of X : x in L } ) by TARSKI:def 4;
consider x being Element of X such that
A6: ( A = IFEQ ((x . O),{},{x},{}) & x in L ) by A5;
A7: x . O = {} by ;
then A = {x} by ;
then a = x by ;
then [x,a] in O1 by A1, A6, A7;
hence a in L | O1 by ; :: thesis: verum