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
( [(Bottom L),x] in a & [(Bottom L),x] in b ) by Def7;
hence [(Bottom L),x] in ab by XBOOLE_0:def 4; :: thesis: verum

end;

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