A3: for d being Element of R st d <<= a & d <<= b holds
min a,b >>= d

proof

let d be Element of R; :: thesis: ( d <<= a & d <<= b implies min a,b >>= d )
assume ( d <<= a & d <<= b ) ; :: thesis: min a,b >>= d
then ( d <= a & d <= b ) by Th3;
then d <= min a,b by XXREAL_0:20;
hence min a,b >>= d by Th3; :: thesis: verum

end;

min a,b <= b by XXREAL_0:17;
then A4: min a,b <<= b by Th3;
min a,b <= a by XXREAL_0:17;
then min a,b <<= a by Th3;
hence a "/\" b = min a,b by A4, A3, YELLOW_0:23; :: thesis: verum