let S, T be non empty reflexive antisymmetric RelStr ; :: thesis: UPS ((id S),(id T)) = id (UPS (S,T))
A1: for x being object st x in the carrier of (UPS (S,T)) holds
(UPS ((id S),(id T))) . x = x

proof

let x be object ; :: thesis: ( x in the carrier of (UPS (S,T)) implies (UPS ((id S),(id T))) . x = x )
assume x in the carrier of (UPS (S,T)) ; :: thesis: (UPS ((id S),(id T))) . x = x
then reconsider f = x as directed-sups-preserving Function of S,T by Def4;
(UPS ((id S),(id T))) . f = ((id T) * f) * (id S) by Def5
.= f * (id S) by FUNCT_2:17 ;
hence (UPS ((id S),(id T))) . x = x by FUNCT_2:17; :: thesis: verum

end;

dom (UPS ((id S),(id T))) = the carrier of (UPS (S,T)) by FUNCT_2:def 1;
hence UPS ((id S),(id T)) = id (UPS (S,T)) by A1, FUNCT_1:17; :: thesis: verum