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