let a, b be object ; :: thesis: ( not a <> b or canFS {a,b} = <*a,b*> or canFS {a,b} = <*b,a*> )
rng (canFS {a,b}) = {a,b} by FUNCT_2:def 3;
hence ( not a <> b or canFS {a,b} = <*a,b*> or canFS {a,b} = <*b,a*> ) by FINSEQ_3:99; :: thesis: verum