defpred S_{1}[ object , object ] means ex x being Element of X st

( $1 = x & $2 in (x . O1) \& O2 );

consider O being Relation such that

A23: for z, s being object holds

( [z,s] in O iff ( z in X & s in X & S_{1}[z,s] ) )
from RELAT_1:sch 1();

O c= [:X,X:]

take O ; :: thesis: for L being List of X holds L | O = union { ((x . O1) \& O2) where x is Element of X : x in L }

let L be List of X; :: thesis: L | O = union { ((x . O1) \& O2) where x is Element of X : x in L }

thus L | O c= union { ((x . O1) \& O2) where x is Element of X : x in L } :: according to XBOOLE_0:def 10 :: thesis: union { ((x . O1) \& O2) where x is Element of X : x in L } c= L | O

assume z in union { ((x . O1) \& O2) where x is Element of X : x in L } ; :: thesis: z in L | O

then consider Y being set such that

A25: ( z in Y & Y in { ((x . O1) \& O2) where x is Element of X : x in L } ) by TARSKI:def 4;

consider x being Element of X such that

A26: ( Y = (x . O1) \& O2 & x in L ) by A25;

[x,z] in O by A23, A25, A26;

hence z in L | O by A26, RELAT_1:def 13; :: thesis: verum

( $1 = x & $2 in (x . O1) \& O2 );

consider O being Relation such that

A23: for z, s being object holds

( [z,s] in O iff ( z in X & s in X & S

O c= [:X,X:]

proof

then reconsider O = O as Operation of X ;
let z, s be object ; :: according to RELAT_1:def 3 :: thesis: ( not [z,s] in O or [z,s] in [:X,X:] )

assume [z,s] in O ; :: thesis: [z,s] in [:X,X:]

then ( z in X & s in X ) by A23;

hence [z,s] in [:X,X:] by ZFMISC_1:87; :: thesis: verum

end;assume [z,s] in O ; :: thesis: [z,s] in [:X,X:]

then ( z in X & s in X ) by A23;

hence [z,s] in [:X,X:] by ZFMISC_1:87; :: thesis: verum

take O ; :: thesis: for L being List of X holds L | O = union { ((x . O1) \& O2) where x is Element of X : x in L }

let L be List of X; :: thesis: L | O = union { ((x . O1) \& O2) where x is Element of X : x in L }

thus L | O c= union { ((x . O1) \& O2) where x is Element of X : x in L } :: according to XBOOLE_0:def 10 :: thesis: union { ((x . O1) \& 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 union { ((x . O1) \& O2) where x is Element of X : x in L } or z in L | O )
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in L | O or z in union { ((x . O1) \& O2) where x is Element of X : x in L } )

assume z in L | O ; :: thesis: z in union { ((x . O1) \& O2) where x is Element of X : x in L }

then consider y being Element of X such that

A24: ( z in y . O & y in L ) by Th23;

[y,z] in O by A24, RELAT_1:169;

then ex x being Element of X st

( y = x & z in (x . O1) \& O2 ) by A23;

then ( z in (y . O1) \& O2 & (y . O1) \& O2 in { ((x . O1) \& O2) where x is Element of X : x in L } ) by A24;

hence z in union { ((x . O1) \& O2) where x is Element of X : x in L } by TARSKI:def 4; :: thesis: verum

end;assume z in L | O ; :: thesis: z in union { ((x . O1) \& O2) where x is Element of X : x in L }

then consider y being Element of X such that

A24: ( z in y . O & y in L ) by Th23;

[y,z] in O by A24, RELAT_1:169;

then ex x being Element of X st

( y = x & z in (x . O1) \& O2 ) by A23;

then ( z in (y . O1) \& O2 & (y . O1) \& O2 in { ((x . O1) \& O2) where x is Element of X : x in L } ) by A24;

hence z in union { ((x . O1) \& O2) where x is Element of X : x in L } by TARSKI:def 4; :: thesis: verum

assume z in union { ((x . O1) \& O2) where x is Element of X : x in L } ; :: thesis: z in L | O

then consider Y being set such that

A25: ( z in Y & Y in { ((x . O1) \& O2) where x is Element of X : x in L } ) by TARSKI:def 4;

consider x being Element of X such that

A26: ( Y = (x . O1) \& O2 & x in L ) by A25;

[x,z] in O by A23, A25, A26;

hence z in L | O by A26, RELAT_1:def 13; :: thesis: verum