let L be lower-bounded with_suprema Poset; :: thesis: for a, b being auxiliary Relation of holds a /\ b is auxiliary Relation of
let a, b be auxiliary Relation of ; :: thesis: a /\ b is auxiliary Relation of
reconsider ab = a /\ b as Relation of ;
( 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 ; :: thesis: verum