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