let L be lower-bounded with_suprema Poset; :: thesis: for a, b being auxiliary(i) Relation of holds a /\ b is auxiliary(i) Relation of
let a, b be auxiliary(i) Relation of ; :: thesis: a /\ b is auxiliary(i) Relation of
reconsider ab = a /\ b as Relation of ;
for x, y being Element of st [x,y] in ab holds
x <= y

proof

let x, y be Element of ; :: thesis: ( [x,y] in ab implies x <= y )
assume [x,y] in ab ; :: thesis: x <= y
then [x,y] in a by XBOOLE_0:def 4;
hence x <= y by Def4; :: thesis: verum

end;

hence a /\ b is auxiliary(i) Relation of by Def4; :: thesis: verum