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

proof

let x, y, z be Element of L; :: thesis: ( [x,z] in ab & [y,z] in ab implies [(x "\/" y),z] in ab )
assume ( [x,z] in ab & [y,z] in ab ) ; :: thesis: [(x "\/" y),z] in ab
then ( [x,z] in a & [x,z] in b & [y,z] in a & [y,z] in b ) by XBOOLE_0:def 4;
then ( [(x "\/" y),z] in a & [(x "\/" y),z] in b ) by Def6;
hence [(x "\/" y),z] in ab by XBOOLE_0:def 4; :: thesis: verum

end;

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