let L be non empty RelStr ; :: thesis: for Y being Subset of L
for x being Element of L holds {x} "\/" Y = { (x "\/" y) where y is Element of L : y in Y }
let Y be Subset of L; :: thesis: for x being Element of L holds {x} "\/" Y = { (x "\/" y) where y is Element of L : y in Y }
let x be Element of L; :: thesis: {x} "\/" Y = { (x "\/" y) where y is Element of L : y in Y }
thus {x} "\/" Y c= { (x "\/" y) where y is Element of L : y in Y } :: according to XBOOLE_0:def 10 :: thesis: { (x "\/" y) where y is Element of L : y in Y } c= {x} "\/" Y

proof

let q be object ; :: according to TARSKI:def 3 :: thesis: ( not q in {x} "\/" Y or q in { (x "\/" y) where y is Element of L : y in Y } )
assume q in {x} "\/" Y ; :: thesis: q in { (x "\/" y) where y is Element of L : y in Y }
then consider s, t being Element of L such that
A1: q = s "\/" t and
A2: s in {x} and
A3: t in Y ;
s = x by A2, TARSKI:def 1;
hence q in { (x "\/" y) where y is Element of L : y in Y } by A1, A3; :: thesis: verum

end;

let q be object ; :: according to TARSKI:def 3 :: thesis: ( not q in { (x "\/" y) where y is Element of L : y in Y } or q in {x} "\/" Y )
assume q in { (x "\/" y) where y is Element of L : y in Y } ; :: thesis: q in {x} "\/" Y
then A4: ex y being Element of L st
( q = x "\/" y & y in Y ) ;
x in {x} by TARSKI:def 1;
hence q in {x} "\/" Y by A4; :: thesis: verum