let U be set ; :: thesis: for A, B being Subset of U st not A c= B holds

Inter (A,B) = {}

let A, B be Subset of U; :: thesis: ( not A c= B implies Inter (A,B) = {} )

assume A1: not A c= B ; :: thesis: Inter (A,B) = {}

assume Inter (A,B) <> {} ; :: thesis: contradiction

then consider x being object such that

A2: x in Inter (A,B) by XBOOLE_0:def 1;

reconsider x = x as set by TARSKI:1;

( A c= x & x c= B ) by A2, Th1;

hence contradiction by A1; :: thesis: verum

Inter (A,B) = {}

let A, B be Subset of U; :: thesis: ( not A c= B implies Inter (A,B) = {} )

assume A1: not A c= B ; :: thesis: Inter (A,B) = {}

assume Inter (A,B) <> {} ; :: thesis: contradiction

then consider x being object such that

A2: x in Inter (A,B) by XBOOLE_0:def 1;

reconsider x = x as set by TARSKI:1;

( A c= x & x c= B ) by A2, Th1;

hence contradiction by A1; :: thesis: verum