for m, n being Nat st m <> n holds

(Partial_Diff_Union A1) . n misses (Partial_Diff_Union A1) . m

(Partial_Diff_Union A1) . n misses (Partial_Diff_Union A1) . m

proof

hence
Partial_Diff_Union A1 is disjoint_valued
; :: thesis: verum
let m, n be Nat; :: thesis: ( m <> n implies (Partial_Diff_Union A1) . n misses (Partial_Diff_Union A1) . m )

assume A1: m <> n ; :: thesis: (Partial_Diff_Union A1) . n misses (Partial_Diff_Union A1) . m

assume (Partial_Diff_Union A1) . n meets (Partial_Diff_Union A1) . m ; :: thesis: contradiction

then consider x being object such that

A2: x in (Partial_Diff_Union A1) . n and

A3: x in (Partial_Diff_Union A1) . m by XBOOLE_0:3;

end;assume A1: m <> n ; :: thesis: (Partial_Diff_Union A1) . n misses (Partial_Diff_Union A1) . m

assume (Partial_Diff_Union A1) . n meets (Partial_Diff_Union A1) . m ; :: thesis: contradiction

then consider x being object such that

A2: x in (Partial_Diff_Union A1) . n and

A3: x in (Partial_Diff_Union A1) . m by XBOOLE_0:3;

per cases
( m < n or n < m )
by A1, XXREAL_0:1;

end;