union { (x . O) where x is Element of X : x in L } = | L
_{1} being List of X holds

( b_{1} = | L iff b_{1} = union { (x . O) where x is Element of X : x in L } )
; :: thesis: verum

proof

hence
for b
thus
union { (x . O) where x is Element of X : x in L } c= | L
:: according to XBOOLE_0:def 10 :: thesis: | L c= union { (x . O) where x is Element of X : x in L }

end;proof

thus
| L c= union { (x . O) where x is Element of X : x in L }
:: thesis: verum
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in union { (x . O) where x is Element of X : x in L } or z in | L )

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

then consider Y being set such that

A1: ( z in Y & Y in { (x . O) where x is Element of X : x in L } ) by TARSKI:def 4;

consider x being Element of X such that

A2: ( Y = x . O & x in L ) by A1;

[x,z] in O by A1, A2, RELAT_1:169;

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

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

then consider Y being set such that

A1: ( z in Y & Y in { (x . O) where x is Element of X : x in L } ) by TARSKI:def 4;

consider x being Element of X such that

A2: ( Y = x . O & x in L ) by A1;

[x,z] in O by A1, A2, RELAT_1:169;

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

proof

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in | L or z in union { (x . O) where x is Element of X : x in L } )

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

then consider y being object such that

A3: ( [y,z] in O & y in L ) by RELAT_1:def 13;

reconsider y = y as Element of X by A3;

( z in y . O & y . O in { (x . O) where x is Element of X : x in L } ) by A3, RELAT_1:169;

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

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

then consider y being object such that

A3: ( [y,z] in O & y in L ) by RELAT_1:def 13;

reconsider y = y as Element of X by A3;

( z in y . O & y . O in { (x . O) where x is Element of X : x in L } ) by A3, RELAT_1:169;

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

( b