let L be lower-bounded with_suprema Poset; :: thesis: for a, b being auxiliary Relation of L holds a /\ b is auxiliary Relation of L
let a, b be auxiliary Relation of L; :: thesis: a /\ b is auxiliary Relation of L
reconsider ab = a /\ b as Relation of L ;
( ab is auxiliary(i) & ab is auxiliary(ii) & ab is auxiliary(iii) & ab is auxiliary(iv) ) by Th6, Th7, Th8, Th9;
hence a /\ b is auxiliary Relation of L ; :: thesis: verum