let N be non empty Poset; :: thesis: IdsMap N is V13()
set f = IdsMap N;
let x, y be Element of N; :: according to WAYBEL_1:def 1 :: thesis: ( not (IdsMap N) . x = (IdsMap N) . y or x = y )
assume A1: (IdsMap N) . x = (IdsMap N) . y ; :: thesis: x = y
( (IdsMap N) . x = downarrow x & (IdsMap N) . y = downarrow y ) by YELLOW_2:def 4;
hence x = y by A1, WAYBEL_0:19; :: thesis: verum