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, Lemacik;
then X c= Y by XBOOLE_1:1;
hence ( X in Inter X,Y & Y in Inter X,Y ) ; :: thesis: verum