let S be non empty non void ManySortedSign ; :: thesis: for A being non-empty MSAlgebra of 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 of 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 set ; :: 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 set ; :: 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 16;
then reconsider x9 = x9 as Element of (EqRelLatt the Sorts of A) by TARSKI:def 3;
{x9} is finite Subset of X by A5, SUBSET_1:63;
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 set ; :: 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, XBOOLE_0:def 10;

now

let i be set ; :: 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) by TARSKI:def 3;
{ ("\/" 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 set ; :: 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, XBOOLE_0:def 10;
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:49; :: thesis: verum