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 A0: not A c= B ; :: thesis: Inter A,B = {}
assume Inter A,B <> {} ; :: thesis: contradiction
then consider x being set such that
A1: x in Inter A,B by XBOOLE_0:def 1;
( A c= x & x c= B ) by A1, Lemacik;
hence contradiction by A0, XBOOLE_1:1; :: thesis: verum