let S be non void Signature; :: thesis: for A being disjoint_valued MSAlgebra of S
for C1, C2 being Component of the Sorts of A holds
( C1 = C2 or C1 misses C2 )
let A be disjoint_valued MSAlgebra of S; :: thesis: for C1, C2 being Component of the Sorts of A holds
( C1 = C2 or C1 misses C2 )
let C1, C2 be Component of the Sorts of A; :: thesis: ( C1 = C2 or C1 misses C2 )
consider x being set such that
A2: ( x in dom the Sorts of A & C1 = the Sorts of A . x ) by FUNCT_1:def 5;
consider y being set such that
A3: ( y in dom the Sorts of A & C2 = the Sorts of A . y ) by FUNCT_1:def 5;
( the Sorts of A is disjoint_valued & ( x = y or x <> y ) ) by MSAFREE1:def 2;
hence ( C1 = C2 or C1 misses C2 ) by A2, A3, PROB_2:def 3; :: thesis: verum