union { (x . O) where x is Element of X : x in L } = | L
proof
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 }
proof
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;
thus | L c= union { (x . O) where x is Element of X : x in L } :: 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;
end;
hence for b1 being List of X holds
( b1 = | L iff b1 = union { (x . O) where x is Element of X : x in L } ) ; :: thesis: verum