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 object ; :: according to TARSKI:def 3 :: thesis: ( not x in Inter (A,({} U)) or x in {} )
reconsider xx = x as set by TARSKI:1;
assume x in Inter (A,({} U)) ; :: thesis: x in {}
then ( A c= xx & xx c= {} U ) by Th1;
hence x in {} ; :: thesis: verum

end;

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