let x, y be object ; :: thesis: {[x,x]},{[y,y]} are_isomorphic
take x .--> y ; :: according to WELLORD1:def 8 :: thesis: x .--> y is_isomorphism_of {[x,x]},{[y,y]}
thus x .--> y is_isomorphism_of {[x,x]},{[y,y]} by Th82; :: thesis: verum