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 ) )
proof
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;
hence ( X meets Y iff ex v being Element of V st
( v in X & v in Y ) ) by XBOOLE_0:3; :: thesis: verum