let R be 1-sorted ; :: thesis: for X being Subset of R holds { x where x is Element of R : {} meets X } = {} R
let X be Subset of R; :: thesis: { x where x is Element of R : {} meets X } = {} R
thus { x where x is Element of R : {} meets X } c= {} R :: according to XBOOLE_0:def 10 :: thesis: {} R c= { x where x is Element of R : {} meets X }
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in { x where x is Element of R : {} meets X } or y in {} R )
assume y in { x where x is Element of R : {} meets X } ; :: thesis: y in {} R
then ex z being Element of R st
( z = y & {} meets X ) ;
then {} /\ X <> {} ;
hence y in {} R ; :: thesis: verum
end;
thus {} R c= { x where x is Element of R : {} meets X } ; :: thesis: verum