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 object such that

A1: x in Inter (X,Y) by XBOOLE_0:def 1;

reconsider x = x as set by TARSKI:1;

( X c= x & x c= Y ) by A1, Th1;

then X c= Y ;

hence ( X in Inter (X,Y) & Y in Inter (X,Y) ) ; :: thesis: verum

( 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 object such that

A1: x in Inter (X,Y) by XBOOLE_0:def 1;

reconsider x = x as set by TARSKI:1;

( X c= x & x c= Y ) by A1, Th1;

then X c= Y ;

hence ( X in Inter (X,Y) & Y in Inter (X,Y) ) ; :: thesis: verum