let U be non empty set ; :: thesis: for A being non empty Subset of U holds Inter A,({} U) = {}
let A be non empty Subset of U; :: thesis: Inter A,({} U) = {}
thus Inter A,({} U) c= {} :: according to XBOOLE_0:def 10 :: thesis: {} c= Inter A,({} U)

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in Inter A,({} U) or x in {} )
assume x in Inter A,({} U) ; :: thesis: x in {}
then ( A c= x & x c= {} U ) by Lemacik;
hence x in {} ; :: thesis: verum

end;

thus {} c= Inter A,({} U) by XBOOLE_1:2; :: thesis: verum