let x, y be object ; for k being Nat st Seg k = {x,y} & x <> y holds
( k = 2 & {x,y} = {1,2} )
let k be Nat; ( Seg k = {x,y} & x <> y implies ( k = 2 & {x,y} = {1,2} ) )
assume that
A1:
Seg k = {x,y}
and
A2:
x <> y
; ( k = 2 & {x,y} = {1,2} )
hence
( k = 2 & {x,y} = {1,2} )
; verum