set F = FreeSort X;
let x, y be set ; :: according to PROB_2:def 3 :: thesis: ( x = y or (FreeSort X) . x misses (FreeSort X) . y )

per cases ( ( x in dom (FreeSort X) & y in dom (FreeSort X) ) or not x in dom (FreeSort X) or not y in dom (FreeSort X) ) ;

suppose ( x in dom (FreeSort X) & y in dom (FreeSort X) ) ; :: thesis: ( x = y or (FreeSort X) . x misses (FreeSort X) . y )

then reconsider s1 = x, s2 = y as SortSymbol of S by PARTFUN1:def 4;
assume x <> y ; :: thesis: (FreeSort X) . x misses (FreeSort X) . y
then (FreeSort X) . s1 misses (FreeSort X) . s2 by MSAFREE:13;
hence (FreeSort X) . x misses (FreeSort X) . y ; :: thesis: verum

end;

suppose A1: ( not x in dom (FreeSort X) or not y in dom (FreeSort X) ) ; :: thesis: ( x = y or (FreeSort X) . x misses (FreeSort X) . y )

assume x <> y ; :: thesis: (FreeSort X) . x misses (FreeSort X) . y
( (FreeSort X) . x = {} or (FreeSort X) . y = {} ) by A1, FUNCT_1:def 4;
hence (FreeSort X) . x misses (FreeSort X) . y by XBOOLE_1:65; :: thesis: verum

end;

end;