let U be set ; :: thesis: for A, B being Subset of U st Inter (A,B) <> {} holds
A c= B
let A, B be Subset of U; :: thesis: ( Inter (A,B) <> {} implies A c= B )
assume Inter (A,B) <> {} ; :: thesis: A c= B
then consider x being object such that
A1: 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 A1, Th1;
hence A c= B ; :: thesis: verum