for x, y being set st x in Aux L & y in Aux L holds
x /\ y in Aux L

proof

let x, y be set ; :: thesis: ( x in Aux L & y in Aux L implies x /\ y in Aux L )
assume ( x in Aux L & y in Aux L ) ; :: thesis: x /\ y in Aux L
then ( x is auxiliary Relation of L & y is auxiliary Relation of L ) by Def9;
then x /\ y is auxiliary Relation of L by Th10;
hence x /\ y in Aux L by Def9; :: thesis: verum

end;

hence InclPoset (Aux L) is with_infima by YELLOW_1:12; :: thesis: verum