let X be non empty set ; :: thesis: for S, T being non empty Poset holds UPS S,(T |^ X),(UPS S,T) |^ X are_isomorphic
let S, T be non empty Poset; :: thesis: UPS S,(T |^ X),(UPS S,T) |^ X are_isomorphic
consider F being Function of (UPS S,(T |^ X)),((UPS S,T) |^ X) such that
A1: ( F is commuting & F is isomorphic ) by Th41;
take F ; :: according to WAYBEL_1:def 8 :: thesis: F is isomorphic
thus F is isomorphic by A1; :: thesis: verum