let S be non empty non void ManySortedSign ; :: thesis: for A being non-empty MSAlgebra of S
for B1, B2 being Subset of (CongrLatt A)
for C1, C2 being MSCongruence of A st C1 = "\/" B1,(EqRelLatt the Sorts of A) & C2 = "\/" B2,(EqRelLatt the Sorts of A) holds
C1 "\/" C2 = "\/" (B1 \/ B2),(EqRelLatt the Sorts of A)
let A be non-empty MSAlgebra of S; :: thesis: for B1, B2 being Subset of (CongrLatt A)
for C1, C2 being MSCongruence of A st C1 = "\/" B1,(EqRelLatt the Sorts of A) & C2 = "\/" B2,(EqRelLatt the Sorts of A) holds
C1 "\/" C2 = "\/" (B1 \/ B2),(EqRelLatt the Sorts of A)
let B1, B2 be Subset of (CongrLatt A); :: thesis: for C1, C2 being MSCongruence of A st C1 = "\/" B1,(EqRelLatt the Sorts of A) & C2 = "\/" B2,(EqRelLatt the Sorts of A) holds
C1 "\/" C2 = "\/" (B1 \/ B2),(EqRelLatt the Sorts of A)
let C1, C2 be MSCongruence of A; :: thesis: ( C1 = "\/" B1,(EqRelLatt the Sorts of A) & C2 = "\/" B2,(EqRelLatt the Sorts of A) implies C1 "\/" C2 = "\/" (B1 \/ B2),(EqRelLatt the Sorts of A) )
set C = EqRelLatt the Sorts of A;
assume A1: ( C1 = "\/" B1,(EqRelLatt the Sorts of A) & C2 = "\/" B2,(EqRelLatt the Sorts of A) ) ; :: thesis: C1 "\/" C2 = "\/" (B1 \/ B2),(EqRelLatt the Sorts of A)
the carrier of (CongrLatt A) c= the carrier of (EqRelLatt the Sorts of A) by NAT_LAT:def 16;
then reconsider D1 = B1, D2 = B2 as Subset of (EqRelLatt the Sorts of A) by XBOOLE_1:1;
A2: {("\/" D1),("\/" D2)} c= { ("\/" Y) where Y is Subset of (EqRelLatt the Sorts of A) : Y in {B1,B2} }

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in {("\/" D1),("\/" D2)} or x in { ("\/" Y) where Y is Subset of (EqRelLatt the Sorts of A) : Y in {B1,B2} } )
assume x in {("\/" D1),("\/" D2)} ; :: thesis: x in { ("\/" Y) where Y is Subset of (EqRelLatt the Sorts of A) : Y in {B1,B2} }
then A3: ( x = "\/" D1 or x = "\/" D2 ) by TARSKI:def 2;
( D1 in {B1,B2} & D2 in {B1,B2} ) by TARSKI:def 2;
hence x in { ("\/" Y) where Y is Subset of (EqRelLatt the Sorts of A) : Y in {B1,B2} } by A3; :: thesis: verum

end;

{ ("\/" Y) where Y is Subset of (EqRelLatt the Sorts of A) : Y in {B1,B2} } c= {("\/" D1),("\/" D2)}

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { ("\/" Y) where Y is Subset of (EqRelLatt the Sorts of A) : Y in {B1,B2} } or x in {("\/" D1),("\/" D2)} )
assume x in { ("\/" Y) where Y is Subset of (EqRelLatt the Sorts of A) : Y in {B1,B2} } ; :: thesis: x in {("\/" D1),("\/" D2)}
then consider X1 being Subset of (EqRelLatt the Sorts of A) such that
A4: x = "\/" X1 and
A5: X1 in {B1,B2} ;
( X1 = B1 or X1 = B2 ) by A5, TARSKI:def 2;
hence x in {("\/" D1),("\/" D2)} by A4, TARSKI:def 2; :: thesis: verum

end;

then A6: { ("\/" Y) where Y is Subset of (EqRelLatt the Sorts of A) : Y in {B1,B2} } = {("\/" D1),("\/" D2)} by A2, XBOOLE_0:def 10;

now

let i be set ; :: thesis: ( i in {B1,B2} implies i in bool the carrier of (EqRelLatt the Sorts of A) )
assume i in {B1,B2} ; :: thesis: i in bool the carrier of (EqRelLatt the Sorts of A)
then ( i = D1 or i = D2 ) by TARSKI:def 2;
hence i in bool the carrier of (EqRelLatt the Sorts of A) ; :: thesis: verum

end;

then A7: {B1,B2} c= bool the carrier of (EqRelLatt the Sorts of A) by TARSKI:def 3;
thus "\/" (B1 \/ B2),(EqRelLatt the Sorts of A) = "\/" (union {B1,B2}),(EqRelLatt the Sorts of A) by ZFMISC_1:93
.= "\/" { ("\/" Y) where Y is Subset of (EqRelLatt the Sorts of A) : Y in {B1,B2} } ,(EqRelLatt the Sorts of A) by A7, LATTICE3:49
.= ("\/" D1) "\/" ("\/" D2) by A6, LATTICE3:44
.= the L_join of (EqRelLatt the Sorts of A) . C1,C2 by A1, LATTICES:def 1
.= C1 "\/" C2 by MSUALG_5:def 5 ; :: thesis: verum