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 ) )

then x is Subset of U by XBOOLE_1:1;

hence x in Inter (X,Y) by A2; :: thesis: verum

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 A2:
( X c= x & x c= Y )
; :: thesis: 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;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

then x is Subset of U by XBOOLE_1:1;

hence x in Inter (X,Y) by A2; :: thesis: verum