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))

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

thus
{} c= Inter (A,({} U))
; :: thesis: verum
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;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