let S be non empty non void ManySortedSign ; :: thesis: for A being non-empty MSAlgebra over S
for X being Subset of (CongrLatt A) holds "\/" (X,(EqRelLatt the Sorts of A)) = "\/" ( { ("\/" (X0,(EqRelLatt the Sorts of A))) where X0 is Subset of (EqRelLatt the Sorts of A) : X0 is finite Subset of X } ,(EqRelLatt the Sorts of A))
let A be non-empty MSAlgebra over S; :: thesis: for X being Subset of (CongrLatt A) holds "\/" (X,(EqRelLatt the Sorts of A)) = "\/" ( { ("\/" (X0,(EqRelLatt the Sorts of A))) where X0 is Subset of (EqRelLatt the Sorts of A) : X0 is finite Subset of X } ,(EqRelLatt the Sorts of A))
let X be Subset of (CongrLatt A); :: thesis: "\/" (X,(EqRelLatt the Sorts of A)) = "\/" ( { ("\/" (X0,(EqRelLatt the Sorts of A))) where X0 is Subset of (EqRelLatt the Sorts of A) : X0 is finite Subset of X } ,(EqRelLatt the Sorts of A))
set E = EqRelLatt the Sorts of A;
set X1 = { X0 where X0 is Subset of (EqRelLatt the Sorts of A) : X0 is finite Subset of X } ;
set B1 = { ("\/" Y) where Y is Subset of (EqRelLatt the Sorts of A) : Y in { X0 where X0 is Subset of (EqRelLatt the Sorts of A) : X0 is finite Subset of X } } ;
set B2 = { ("\/" (X0,(EqRelLatt the Sorts of A))) where X0 is Subset of (EqRelLatt the Sorts of A) : X0 is finite Subset of X } ;
A1: { ("\/" (X0,(EqRelLatt the Sorts of A))) where X0 is Subset of (EqRelLatt the Sorts of A) : X0 is finite Subset of X } c= { ("\/" Y) where Y is Subset of (EqRelLatt the Sorts of A) : Y in { X0 where X0 is Subset of (EqRelLatt the Sorts of A) : X0 is finite Subset of X } }

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { ("\/" (X0,(EqRelLatt the Sorts of A))) where X0 is Subset of (EqRelLatt the Sorts of A) : X0 is finite Subset of X } or x in { ("\/" Y) where Y is Subset of (EqRelLatt the Sorts of A) : Y in { X0 where X0 is Subset of (EqRelLatt the Sorts of A) : X0 is finite Subset of X } } )
assume x in { ("\/" (X0,(EqRelLatt the Sorts of A))) where X0 is Subset of (EqRelLatt the Sorts of A) : X0 is finite Subset of X } ; :: thesis: x in { ("\/" Y) where Y is Subset of (EqRelLatt the Sorts of A) : Y in { X0 where X0 is Subset of (EqRelLatt the Sorts of A) : X0 is finite Subset of X } }
then consider Y1 being Subset of (EqRelLatt the Sorts of A) such that
A2: x = "\/" Y1 and
A3: Y1 is finite Subset of X ;
Y1 in { X0 where X0 is Subset of (EqRelLatt the Sorts of A) : X0 is finite Subset of X } by A3;
hence x in { ("\/" Y) where Y is Subset of (EqRelLatt the Sorts of A) : Y in { X0 where X0 is Subset of (EqRelLatt the Sorts of A) : X0 is finite Subset of X } } by A2; :: thesis: verum

end;

A4: X c= union { X0 where X0 is Subset of (EqRelLatt the Sorts of A) : X0 is finite Subset of X }

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in X or x in union { X0 where X0 is Subset of (EqRelLatt the Sorts of A) : X0 is finite Subset of X } )
assume A5: x in X ; :: thesis: x in union { X0 where X0 is Subset of (EqRelLatt the Sorts of A) : X0 is finite Subset of X }
then reconsider x9 = x as Element of (CongrLatt A) ;
the carrier of (CongrLatt A) c= the carrier of (EqRelLatt the Sorts of A) by NAT_LAT:def 12;
then reconsider x9 = x9 as Element of (EqRelLatt the Sorts of A) ;
{x9} is finite Subset of X by A5, SUBSET_1:41;
then ( x in {x} & {x9} in { X0 where X0 is Subset of (EqRelLatt the Sorts of A) : X0 is finite Subset of X } ) by TARSKI:def 1;
hence x in union { X0 where X0 is Subset of (EqRelLatt the Sorts of A) : X0 is finite Subset of X } by TARSKI:def 4; :: thesis: verum

end;

union { X0 where X0 is Subset of (EqRelLatt the Sorts of A) : X0 is finite Subset of X } c= X

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in union { X0 where X0 is Subset of (EqRelLatt the Sorts of A) : X0 is finite Subset of X } or x in X )
assume x in union { X0 where X0 is Subset of (EqRelLatt the Sorts of A) : X0 is finite Subset of X } ; :: thesis: x in X
then consider Y1 being set such that
A6: x in Y1 and
A7: Y1 in { X0 where X0 is Subset of (EqRelLatt the Sorts of A) : X0 is finite Subset of X } by TARSKI:def 4;
ex Y2 being Subset of (EqRelLatt the Sorts of A) st
( Y1 = Y2 & Y2 is finite Subset of X ) by A7;
hence x in X by A6; :: thesis: verum

end;

then A8: X = union { X0 where X0 is Subset of (EqRelLatt the Sorts of A) : X0 is finite Subset of X } by A4;

now :: thesis: for i being object st i in { X0 where X0 is Subset of (EqRelLatt the Sorts of A) : X0 is finite Subset of X } holds
i in bool the carrier of (EqRelLatt the Sorts of A)

let i be object ; :: thesis: ( i in { X0 where X0 is Subset of (EqRelLatt the Sorts of A) : X0 is finite Subset of X } implies i in bool the carrier of (EqRelLatt the Sorts of A) )
assume i in { X0 where X0 is Subset of (EqRelLatt the Sorts of A) : X0 is finite Subset of X } ; :: thesis: i in bool the carrier of (EqRelLatt the Sorts of A)
then ex I1 being Subset of (EqRelLatt the Sorts of A) st
( i = I1 & I1 is finite Subset of X ) ;
hence i in bool the carrier of (EqRelLatt the Sorts of A) ; :: thesis: verum

end;

then A9: { X0 where X0 is Subset of (EqRelLatt the Sorts of A) : X0 is finite Subset of X } c= bool the carrier of (EqRelLatt the Sorts of A) ;
{ ("\/" Y) where Y is Subset of (EqRelLatt the Sorts of A) : Y in { X0 where X0 is Subset of (EqRelLatt the Sorts of A) : X0 is finite Subset of X } } c= { ("\/" (X0,(EqRelLatt the Sorts of A))) where X0 is Subset of (EqRelLatt the Sorts of A) : X0 is finite Subset of X }

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 { X0 where X0 is Subset of (EqRelLatt the Sorts of A) : X0 is finite Subset of X } } or x in { ("\/" (X0,(EqRelLatt the Sorts of A))) where X0 is Subset of (EqRelLatt the Sorts of A) : X0 is finite Subset of X } )
assume x in { ("\/" Y) where Y is Subset of (EqRelLatt the Sorts of A) : Y in { X0 where X0 is Subset of (EqRelLatt the Sorts of A) : X0 is finite Subset of X } } ; :: thesis: x in { ("\/" (X0,(EqRelLatt the Sorts of A))) where X0 is Subset of (EqRelLatt the Sorts of A) : X0 is finite Subset of X }
then consider Y1 being Subset of (EqRelLatt the Sorts of A) such that
A10: x = "\/" Y1 and
A11: Y1 in { X0 where X0 is Subset of (EqRelLatt the Sorts of A) : X0 is finite Subset of X } ;
ex Y2 being Subset of (EqRelLatt the Sorts of A) st
( Y1 = Y2 & Y2 is finite Subset of X ) by A11;
hence x in { ("\/" (X0,(EqRelLatt the Sorts of A))) where X0 is Subset of (EqRelLatt the Sorts of A) : X0 is finite Subset of X } by A10; :: thesis: verum

end;

then { ("\/" Y) where Y is Subset of (EqRelLatt the Sorts of A) : Y in { X0 where X0 is Subset of (EqRelLatt the Sorts of A) : X0 is finite Subset of X } } = { ("\/" (X0,(EqRelLatt the Sorts of A))) where X0 is Subset of (EqRelLatt the Sorts of A) : X0 is finite Subset of X } by A1;
hence "\/" (X,(EqRelLatt the Sorts of A)) = "\/" ( { ("\/" (X0,(EqRelLatt the Sorts of A))) where X0 is Subset of (EqRelLatt the Sorts of A) : X0 is finite Subset of X } ,(EqRelLatt the Sorts of A)) by A9, A8, LATTICE3:48; :: thesis: verum