let T be 1-sorted ; :: thesis: for A, B being Subset of T holds
( A meets B ` iff A \ B <> {} )
let A, B be Subset of T; :: thesis: ( A meets B ` iff A \ B <> {} )

hereby :: thesis: ( A \ B <> {} implies A meets B ` )

assume A meets B ` ; :: thesis: A \ B <> {}
then A /\ (B `) <> {} by XBOOLE_0:def 7;
hence A \ B <> {} by SUBSET_1:13; :: thesis: verum

end;

assume A \ B <> {} ; :: thesis: A meets B `
then A /\ (B `) <> {} by SUBSET_1:13;
hence A meets B ` by XBOOLE_0:def 7; :: thesis: verum