let A be Ordinal; :: thesis: inf {A} = A
thus inf {A} = meet {A} by Th7
.= A by SETFAM_1:10 ; :: thesis: verum