let X be functional set ; :: thesis: meet X is Function

per cases ( X <> {} or X = {} ) ;

suppose A1: X <> {} ; :: thesis: meet X is Function

consider Z being object such that
A2: Z in X by A1, XBOOLE_0:def 1;
reconsider Z = Z as set by TARSKI:1;

A3: now :: thesis: for x being object st x in meet X holds
ex y, z being object st x = [y,z]

let x be object ; :: thesis: ( x in meet X implies ex y, z being object st x = [y,z] )
assume x in meet X ; :: thesis: ex y, z being object st x = [y,z]
then x in Z by A2, SETFAM_1:def 1;
then consider y, z being object such that
A4: x = [y,z] by A2, RELAT_1:def 1;
take y = y; :: thesis: ex z being object st x = [y,z]
take z = z; :: thesis: x = [y,z]
thus x = [y,z] by A4; :: thesis: verum

end;

now :: thesis: for x, y1, y2 being object st [x,y1] in meet X & [x,y2] in meet X holds
y1 = y2

let x, y1, y2 be object ; :: thesis: ( [x,y1] in meet X & [x,y2] in meet X implies y1 = y2 )
assume ( [x,y1] in meet X & [x,y2] in meet X ) ; :: thesis: y1 = y2
then ( [x,y1] in Z & [x,y2] in Z ) by A2, SETFAM_1:def 1;
hence y1 = y2 by A2, FUNCT_1:def 1; :: thesis: verum

end;

hence meet X is Function by A3, RELAT_1:def 1, FUNCT_1:def 1; :: thesis: verum

end;

suppose X = {} ; :: thesis: meet X is Function

hence meet X is Function by SETFAM_1:def 1; :: thesis: verum

end;

end;