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 } ;

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 consider I1 being Subset of (EqRelLatt the Sorts of A) such that
A1: ( i = I1 & I1 is finite Subset of X ) ;
thus i in bool the carrier of (EqRelLatt the Sorts of A) by A1; :: thesis: verum

end;

then A2: { 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;
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 } ;
A3: { ("\/" 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 }

proof

thus { ("\/" 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 } :: according to XBOOLE_0:def 10 :: thesis: { ("\/" 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 { ("\/" 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
A4: ( x = "\/" Y1 & Y1 in { X0 where X0 is Subset of (EqRelLatt the Sorts of A) : X0 is finite Subset of X } ) ;
consider Y2 being Subset of (EqRelLatt the Sorts of A) such that
A5: ( Y1 = Y2 & Y2 is finite Subset of X ) by A4;
thus 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 A4, A5; :: thesis: verum

end;

thus { ("\/" 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 } } :: thesis: verum

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
A6: ( x = "\/" Y1 & 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 A6;
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 A6; :: thesis: verum

end;

end;

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

proof

thus X c= union { X0 where X0 is Subset of (EqRelLatt the Sorts of A) : X0 is finite Subset of X } :: according to XBOOLE_0:def 10 :: thesis: 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 X or x in union { X0 where X0 is Subset of (EqRelLatt the Sorts of A) : X0 is finite Subset of X } )
assume A7: 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 x' = 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 x' = x' as Element of (EqRelLatt the Sorts of A) by TARSKI:def 3;
A8: x in {x} by TARSKI:def 1;
{x'} is finite Subset of X by A7, SUBSET_1:63;
then {x'} in { X0 where X0 is Subset of (EqRelLatt the Sorts of A) : X0 is finite Subset of X } ;
hence x in union { X0 where X0 is Subset of (EqRelLatt the Sorts of A) : X0 is finite Subset of X } by A8, TARSKI:def 4; :: thesis: verum

end;

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

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
A9: ( x in Y1 & Y1 in { X0 where X0 is Subset of (EqRelLatt the Sorts of A) : X0 is finite Subset of X } ) by TARSKI:def 4;
consider Y2 being Subset of (EqRelLatt the Sorts of A) such that
A10: ( Y1 = Y2 & Y2 is finite Subset of X ) by A9;
thus x in X by A9, A10; :: thesis: verum

end;

end;

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 A2, A3, LATTICE3:49; :: thesis: verum