thus ( S <> {} implies ex f being Function ex A being non empty functional set st
( A = S & dom f = meet { (dom x) where x is Element of A : verum } & ( for i being set st i in dom f holds
f . i = { (x . i) where x is Element of A : verum } ) ) ) :: thesis: ( not S <> {} implies ex b₁ being Function st b₁ = {} )

proof

assume S <> {} ; :: thesis: ex f being Function ex A being non empty functional set st
( A = S & dom f = meet { (dom x) where x is Element of A : verum } & ( for i being set st i in dom f holds
f . i = { (x . i) where x is Element of A : verum } ) )
then consider A being non empty functional set such that
A1: A = S ;
deffunc H₁( object ) -> set = { (x . $1) where x is Element of A : verum } ;
consider f being Function such that
A2: ( dom f = meet { (dom x) where x is Element of A : verum } & ( for i being object st i in meet { (dom x) where x is Element of A : verum } holds
f . i = H₁(i) ) ) from FUNCT_1:sch 3();
take f ; :: thesis: ex A being non empty functional set st
( A = S & dom f = meet { (dom x) where x is Element of A : verum } & ( for i being set st i in dom f holds
f . i = { (x . i) where x is Element of A : verum } ) )
take A ; :: thesis: ( A = S & dom f = meet { (dom x) where x is Element of A : verum } & ( for i being set st i in dom f holds
f . i = { (x . i) where x is Element of A : verum } ) )
thus ( A = S & dom f = meet { (dom x) where x is Element of A : verum } & ( for i being set st i in dom f holds
f . i = { (x . i) where x is Element of A : verum } ) ) by A1, A2; :: thesis: verum

end;

thus ( not S <> {} implies ex b₁ being Function st b₁ = {} ) ; :: thesis: verum