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

proof

let x, y be Element of L; :: 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 Def3; :: thesis: verum

end;

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