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 that
A1: x in Aux L and
A2: y in Aux L ; :: thesis: x /\ y in Aux L
A3: x is auxiliary Relation of L by A1, Def8;
y is auxiliary Relation of L by A2, Def8;
then x /\ y is auxiliary Relation of L by A3, Th10;
hence x /\ y in Aux L by Def8; :: thesis: verum

end;

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