let L be non empty complete Poset; :: thesis: for A, B being non empty Subset of L holds inf (A "/\" B) = (inf A) "/\" (inf B)
let A, B be non empty Subset of L; :: thesis: inf (A "/\" B) = (inf A) "/\" (inf B)
B is_>=_than inf (A "/\" B) by Th54;
then A1: inf B >= inf (A "/\" B) by YELLOW_0:33;
A is_>=_than inf (A "/\" B) by Th54;
then inf A >= inf (A "/\" B) by YELLOW_0:33;
then A2: (inf A) "/\" (inf B) >= (inf (A "/\" B)) "/\" (inf (A "/\" B)) by A1, YELLOW_3:2;
( A is_>=_than inf A & B is_>=_than inf B ) by YELLOW_0:33;
then ( ex_inf_of A "/\" B,L & A "/\" B is_>=_than (inf A) "/\" (inf B) ) by Th55, YELLOW_0:17;
then A3: inf (A "/\" B) >= (inf A) "/\" (inf B) by YELLOW_0:def 10;
(inf (A "/\" B)) "/\" (inf (A "/\" B)) = inf (A "/\" B) by YELLOW_0:25;
hence inf (A "/\" B) = (inf A) "/\" (inf B) by A3, A2, ORDERS_2:2; :: thesis: verum