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