let L be antisymmetric RelStr ; :: thesis:
let a, b, c be Element of L; :: thesis:

hereby :: thesis:

assume that
A1: c = a "/\" b and
A2: ex_inf_of {a,b},L ; :: thesis:
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;

A5: now :: thesis:

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

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:

end;

assume that
A6: ( c <= a & c <= b ) and
A7: for d being Element of L st d <= a & d <= b holds
c >= d ; :: thesis:
thus c = a "/\" b by A6, A7, LATTICE3:def 14; :: thesis:

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

end;

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