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 & [x,y] in b ) by XBOOLE_0:def 4;
hence x <= y by Def4; :: thesis: verum

end;

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