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

proof

let x, y, z be Element of ; :: thesis: ( [x,z] in ab & [y,z] in ab implies [(x "\/" y),z] in ab )
assume that
A1: [x,z] in ab and
A2: [y,z] in ab ; :: thesis: [(x "\/" y),z] in ab
A3: [x,z] in a by A1, XBOOLE_0:def 4;
A4: [x,z] in b by A1, XBOOLE_0:def 4;
A5: [y,z] in a by A2, XBOOLE_0:def 4;
A6: [y,z] in b by A2, XBOOLE_0:def 4;
A7: [(x "\/" y),z] in a by A3, A5, Def6;
[(x "\/" y),z] in b by A4, A6, Def6;
hence [(x "\/" y),z] in ab by A7, XBOOLE_0:def 4; :: thesis: verum

end;

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