let S be non empty non void ManySortedSign ; for A being non-empty MSAlgebra over 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 over 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 B1, B2 be 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 C1, C2 be MSCongruence of A; ( 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)) )
; 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 12;
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} }
{ ("\/" Y) where Y is Subset of (EqRelLatt the Sorts of A) : Y in {B1,B2} } c= {("\/" D1),("\/" D2)}
then A6:
{ ("\/" Y) where Y is Subset of (EqRelLatt the Sorts of A) : Y in {B1,B2} } = {("\/" D1),("\/" D2)}
by A2;
then A7:
{B1,B2} c= bool the carrier of (EqRelLatt the Sorts of A)
;
thus "\/" ((B1 \/ B2),(EqRelLatt the Sorts of A)) =
"\/" ((union {B1,B2}),(EqRelLatt the Sorts of A))
by ZFMISC_1:75
.=
"\/" ( { ("\/" Y) where Y is Subset of (EqRelLatt the Sorts of A) : Y in {B1,B2} } ,(EqRelLatt the Sorts of A))
by A7, LATTICE3:48
.=
("\/" D1) "\/" ("\/" D2)
by A6, LATTICE3:43
.=
the L_join of (EqRelLatt the Sorts of A) . (C1,C2)
by A1, LATTICES:def 1
.=
C1 "\/" C2
by MSUALG_5:def 5
; verum