let X, Y be non empty set ; :: thesis: for A, B being Subset of X
for f being Function of X,Y st f .: A misses f .: B holds
A misses B
let A, B be Subset of X; :: thesis: for f being Function of X,Y st f .: A misses f .: B holds
A misses B
let f be Function of X,Y; :: thesis: ( f .: A misses f .: B implies A misses B )
assume A1: (f .: A) /\ (f .: B) = {} ; :: according to XBOOLE_0:def 7 :: thesis: A misses B
assume A /\ B <> {} ; :: according to XBOOLE_0:def 7 :: thesis: contradiction
then consider x being Element of X such that
A2: x in A /\ B by SUBSET_1:4;
x in B by A2, XBOOLE_0:def 4;
then A3: f . x in f .: B by FUNCT_2:35;
x in A by A2, XBOOLE_0:def 4;
then f . x in f .: A by FUNCT_2:35;
hence contradiction by A1, A3, XBOOLE_0:def 4; :: thesis: verum