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

proof

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

end;

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