let x, y be object ; :: according to PROB_2:def 2 :: thesis: ( x = y or (FreeSort X) . x misses (FreeSort X) . y )
set F = FreeSort X;
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 2;
assume x <> y ; :: thesis: (FreeSort X) . x misses (FreeSort X) . y
then (FreeSort X) . s1 misses (FreeSort X) . s2 by MSAFREE:12;
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 2;
hence (FreeSort X) . x misses (FreeSort X) . y by XBOOLE_1:65; :: thesis: verum
end;
end;