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

proof

let x be Element of ; :: thesis: [(Bottom L),x] in ab
A1: [(Bottom L),x] in a by Def7;
[(Bottom L),x] in b by Def7;
hence [(Bottom L),x] in ab by A1, XBOOLE_0:def 4; :: thesis: verum

end;

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