let y be object ; :: thesis: for R being Relation
for x being object st x in R & y in R & x `1 = y `1 & x `2 = y `2 holds
x = y
let R be Relation; :: thesis: for x being object st x in R & y in R & x `1 = y `1 & x `2 = y `2 holds
x = y
let x be object ; :: thesis: ( x in R & y in R & x `1 = y `1 & x `2 = y `2 implies x = y )
assume ( x in R & y in R ) ; :: thesis: ( not x `1 = y `1 or not x `2 = y `2 or x = y )
then ( x = [(x `1),(x `2)] & y = [(y `1),(y `2)] ) by Th15;
hence ( not x `1 = y `1 or not x `2 = y `2 or x = y ) ; :: thesis: verum