let S be non empty non void ManySortedSign ; :: thesis: 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; :: 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 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} }
proof
let x be object ; :: 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 object ; :: 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;
now :: thesis: for i being object st i in {B1,B2} holds
i in bool the carrier of (EqRelLatt the Sorts of A)
let i be object ; :: 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) ;
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 ; :: thesis: verum