let L be non empty RelStr ; :: thesis: for X being Subset of L holds X "\/" ({} L) = {}
let X be Subset of L; :: thesis: X "\/" ({} L) = {}
thus X "\/" ({} L) c= {} :: according to XBOOLE_0:def 10 :: thesis: {} c= X "\/" ({} L)

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in X "\/" ({} L) or a in {} )
assume a in X "\/" ({} L) ; :: thesis: a in {}
then ex s, t being Element of L st
( a = s "\/" t & s in X & t in {} L ) ;
hence a in {} ; :: thesis: verum

end;

thus {} c= X "\/" ({} L) ; :: thesis: verum