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 set ; :: according to TARSKI:def 3 :: thesis: ( not a in X "/\" ({} L) or a in {} )
assume a in X "/\" ({} L) ; :: thesis: a in {}
then consider s, t being Element of L such that
A1: ( a = s "/\" t & s in X & t in {} L ) ;
thus a in {} by A1; :: thesis: verum

end;

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