set D = { (divs (lamb,x,X,Inv)) where lamb is Element of Lamb : lamb in Lamb } ;
take U = union { (divs (lamb,x,X,Inv)) where lamb is Element of Lamb : lamb in Lamb } ; for o being object holds
( o in U iff ex lamb being object st
( lamb in Lamb & o in divs (lamb,x,X,Inv) ) )
let o be object ; ( o in U iff ex lamb being object st
( lamb in Lamb & o in divs (lamb,x,X,Inv) ) )
thus
( o in U implies ex lamb being object st
( lamb in Lamb & o in divs (lamb,x,X,Inv) ) )
( ex lamb being object st
( lamb in Lamb & o in divs (lamb,x,X,Inv) ) implies o in U )proof
assume
o in U
;
ex lamb being object st
( lamb in Lamb & o in divs (lamb,x,X,Inv) )
then consider d being
set such that A1:
(
o in d &
d in { (divs (lamb,x,X,Inv)) where lamb is Element of Lamb : lamb in Lamb } )
by TARSKI:def 4;
ex
l being
Element of
Lamb st
(
d = divs (
l,
x,
X,
Inv) &
l in Lamb )
by A1;
hence
ex
lamb being
object st
(
lamb in Lamb &
o in divs (
lamb,
x,
X,
Inv) )
by A1;
verum
end;
given lamb being object such that A2:
( lamb in Lamb & o in divs (lamb,x,X,Inv) )
; o in U
divs (lamb,x,X,Inv) in { (divs (lamb,x,X,Inv)) where lamb is Element of Lamb : lamb in Lamb }
by A2;
hence
o in U
by A2, TARSKI:def 4; verum