let V be 1-sorted ; :: thesis: for X, Y being Subset of V holds

( X meets Y iff ex v being Element of V st

( v in X & v in Y ) )

let X, Y be Subset of V; :: thesis: ( X meets Y iff ex v being Element of V st

( v in X & v in Y ) )

( X meets Y implies ex v being Element of V st

( v in X & v in Y ) )

( v in X & v in Y ) ) by XBOOLE_0:3; :: thesis: verum

( X meets Y iff ex v being Element of V st

( v in X & v in Y ) )

let X, Y be Subset of V; :: thesis: ( X meets Y iff ex v being Element of V st

( v in X & v in Y ) )

( X meets Y implies ex v being Element of V st

( v in X & v in Y ) )

proof

hence
( X meets Y iff ex v being Element of V st
assume
X meets Y
; :: thesis: ex v being Element of V st

( v in X & v in Y )

then consider z being object such that

A1: z in X and

A2: z in Y by XBOOLE_0:3;

reconsider v = z as Element of V by A1;

take v ; :: thesis: ( v in X & v in Y )

thus ( v in X & v in Y ) by A1, A2; :: thesis: verum

end;( v in X & v in Y )

then consider z being object such that

A1: z in X and

A2: z in Y by XBOOLE_0:3;

reconsider v = z as Element of V by A1;

take v ; :: thesis: ( v in X & v in Y )

thus ( v in X & v in Y ) by A1, A2; :: thesis: verum

( v in X & v in Y ) ) by XBOOLE_0:3; :: thesis: verum