let L be non empty RelStr ; :: thesis: for D being Subset of [:L,L:] holds union { X where X is Subset of L : ex x being Element of L st
( X = {x} "\/" (proj2 D) & x in proj1 D ) } = (proj1 D) "\/" (proj2 D)
let D be Subset of [:L,L:]; :: thesis: union { X where X is Subset of L : ex x being Element of L st
( X = {x} "\/" (proj2 D) & x in proj1 D ) } = (proj1 D) "\/" (proj2 D)
set D1 = proj1 D;
set D2 = proj2 D;
defpred S₁[ set ] means ex x being Element of L st
( $1 = {x} "\/" (proj2 D) & x in proj1 D );
thus union { X where X is Subset of L : S₁[X] } c= (proj1 D) "\/" (proj2 D) :: according to XBOOLE_0:def 10 :: thesis: (proj1 D) "\/" (proj2 D) c= union { X where X is Subset of L : ex x being Element of L st
( X = {x} "\/" (proj2 D) & x in proj1 D ) }

proof

let q be set ; :: according to TARSKI:def 3 :: thesis: ( not q in union { X where X is Subset of L : S₁[X] } or q in (proj1 D) "\/" (proj2 D) )
assume q in union { X where X is Subset of L : S₁[X] } ; :: thesis: q in (proj1 D) "\/" (proj2 D)
then consider w being set such that
A1: q in w and
A2: w in { X where X is Subset of L : S₁[X] } by TARSKI:def 4;
consider e being Subset of L such that
A3: w = e and
A4: S₁[e] by A2;
consider p being Element of L such that
A5: e = {p} "\/" (proj2 D) and
A6: p in proj1 D by A4;
{p} "\/" (proj2 D) = { (p "\/" y) where y is Element of L : y in proj2 D } by Th15;
then ex y being Element of L st
( q = p "\/" y & y in proj2 D ) by A1, A3, A5;
hence q in (proj1 D) "\/" (proj2 D) by A6; :: thesis: verum

end;

let q be set ; :: according to TARSKI:def 3 :: thesis: ( not q in (proj1 D) "\/" (proj2 D) or q in union { X where X is Subset of L : ex x being Element of L st
( X = {x} "\/" (proj2 D) & x in proj1 D ) } )
assume q in (proj1 D) "\/" (proj2 D) ; :: thesis: q in union { X where X is Subset of L : ex x being Element of L st
( X = {x} "\/" (proj2 D) & x in proj1 D ) }
then consider x, y being Element of L such that
A7: q = x "\/" y and
A8: x in proj1 D and
A9: y in proj2 D ;
{x} "\/" (proj2 D) = { (x "\/" d) where d is Element of L : d in proj2 D } by Th15;
then A10: q in {x} "\/" (proj2 D) by A7, A9;
{x} "\/" (proj2 D) in { X where X is Subset of L : S₁[X] } by A8;
hence q in union { X where X is Subset of L : ex x being Element of L st
( X = {x} "\/" (proj2 D) & x in proj1 D ) } by A10, TARSKI:def 4; :: thesis: verum