let U be set ; :: thesis: for X, Y being Subset of U
for x being set holds
( x in Inter (X,Y) iff ( X c= x & x c= Y ) )
let X, Y be Subset of U; :: thesis: for x being set holds
( x in Inter (X,Y) iff ( X c= x & x c= Y ) )
let x be set ; :: thesis: ( x in Inter (X,Y) iff ( X c= x & x c= Y ) )

hereby :: thesis: ( X c= x & x c= Y implies x in Inter (X,Y) )

assume x in Inter (X,Y) ; :: thesis: ( X c= x & x c= Y )
then consider A9 being Element of bool U such that
A1: ( x = A9 & X c= A9 & A9 c= Y ) ;
thus ( X c= x & x c= Y ) by A1; :: thesis: verum

end;

assume A2: ( X c= x & x c= Y ) ; :: thesis: x in Inter (X,Y)
then x is Subset of U by XBOOLE_1:1;
hence x in Inter (X,Y) by A2; :: thesis: verum