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

min (a,b) >>= d

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

min (a,b) >>= d

proof

min (a,b) <= b
by XXREAL_0:17;
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;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

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