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 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, Def5;
[(x "\/" y),z] in b by A4, A6, Def5;
hence [(x "\/" y),z] in ab by A7, XBOOLE_0:def 4; :: thesis: verum

end;

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