let L be antisymmetric RelStr ; :: thesis: for a, b, c being Element of L holds
( c = a "/\" b & ex_inf_of {a,b},L iff ( c <= a & c <= b & ( for d being Element of L st d <= a & d <= b holds
c >= d ) ) )
let a, b, c be Element of L; :: thesis: ( c = a "/\" b & ex_inf_of {a,b},L iff ( c <= a & c <= b & ( for d being Element of L st d <= a & d <= b holds
c >= d ) ) )

hereby :: thesis: ( c <= a & c <= b & ( for d being Element of L st d <= a & d <= b holds
c >= d ) implies ( c = a "/\" b & ex_inf_of {a,b},L ) )

assume that
A1: c = a "/\" b and
A2: ex_inf_of {a,b},L ; :: thesis: ( c <= a & c <= b & ( for d being Element of L st d <= a & d <= b holds
c >= d ) )
consider c1 being Element of L such that
A3: {a,b} is_>=_than c1 and
A4: for d being Element of L st {a,b} is_>=_than d holds
c1 >= d by A2, Th16;

A5: now

let d be Element of L; :: thesis: ( a >= d & b >= d implies c1 >= d )
assume ( a >= d & b >= d ) ; :: thesis: c1 >= d
then {a,b} is_>=_than d by Th8;
hence c1 >= d by A4; :: thesis: verum

end;

( a >= c1 & b >= c1 ) by A3, Th8;
hence ( c <= a & c <= b & ( for d being Element of L st d <= a & d <= b holds
c >= d ) ) by A1, A5, LATTICE3:def 14; :: thesis: verum

end;

assume A6: ( c <= a & c <= b & ( for d being Element of L st d <= a & d <= b holds
c >= d ) ) ; :: thesis: ( c = a "/\" b & ex_inf_of {a,b},L )
hence c = a "/\" b by LATTICE3:def 14; :: thesis: ex_inf_of {a,b},L

now

take c = c; :: thesis: ( c is_<=_than {a,b} & ( for d being Element of L st d is_<=_than {a,b} holds
c >= d ) )
thus c is_<=_than {a,b} by A6, Th8; :: thesis: for d being Element of L st d is_<=_than {a,b} holds
c >= d
let d be Element of L; :: thesis: ( d is_<=_than {a,b} implies c >= d )
assume d is_<=_than {a,b} ; :: thesis: c >= d
then ( d <= a & d <= b ) by Th8;
hence c >= d by A6; :: thesis: verum

end;

hence ex_inf_of {a,b},L by Th16; :: thesis: verum