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 set ; :: 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 & s in {x} & t in Y ) ;
s = x by A1, TARSKI:def 1;
hence q in { (x "\/" y) where y is Element of L : y in Y } by A1; :: thesis: verum

end;

let q be set ; :: 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 consider y being Element of L such that
A2: ( q = x "\/" y & y in Y ) ;
x in {x} by TARSKI:def 1;
hence q in {x} "\/" Y by A2; :: thesis: verum