let U be set ; :: thesis: for X, Y being Subset of U st Inter (X,Y) <> {} holds
( X in Inter (X,Y) & Y in Inter (X,Y) )
let X, Y be Subset of U; :: thesis: ( Inter (X,Y) <> {} implies ( X in Inter (X,Y) & Y in Inter (X,Y) ) )
assume Inter (X,Y) <> {} ; :: thesis: ( X in Inter (X,Y) & Y in Inter (X,Y) )
then consider x being set such that
A1: x in Inter (X,Y) by XBOOLE_0:def 1;
( X c= x & x c= Y ) by A1, Th1;
then X c= Y by XBOOLE_1:1;
hence ( X in Inter (X,Y) & Y in Inter (X,Y) ) ; :: thesis: verum