let X, Y be set ; :: thesis: ( [:X,Y:] <> {} implies for x being Element of [:X,Y:] holds
( x <> x `1 & x <> x `2 ) )
assume [:X,Y:] <> {} ; :: thesis: for x being Element of [:X,Y:] holds
( x <> x `1 & x <> x `2 )
then ( X <> {} & Y <> {} ) by ZFMISC_1:90;
hence for x being Element of [:X,Y:] holds
( x <> x `1 & x <> x `2 ) by Th18; :: thesis: verum