let L be lower-bounded with_suprema Poset; :: thesis: for X being non empty Subset of (InclPoset (Aux L)) holds meet X is auxiliary Relation of L
let X be non empty Subset of (InclPoset (Aux L)); :: thesis: meet X is auxiliary Relation of L
X c= the carrier of (InclPoset (Aux L)) ;
then A1: X c= Aux L by YELLOW_1:1;
set a = the Element of X;
the Element of X in X ;
then the Element of X is auxiliary Relation of L by A1, Def8;
then reconsider ab = meet X as Relation of L by SETFAM_1:7;
A2: ab is auxiliary(i)
proof
let x, y be Element of L; :: according to WAYBEL_4:def 3 :: thesis: ( [x,y] in ab implies x <= y )
assume A3: [x,y] in ab ; :: thesis: x <= y
set V = the Element of X;
A4: the Element of X in X ;
A5: [x,y] in the Element of X by A3, SETFAM_1:def 1;
the Element of X is auxiliary Relation of L by A1, A4, Def8;
hence x <= y by A5, Def3; :: thesis: verum
end;
A6: ab is auxiliary(ii)
proof
let x, y, z, u be Element of L; :: according to WAYBEL_4:def 4 :: thesis: ( u <= x & [x,y] in ab & y <= z implies [u,z] in ab )
assume that
A7: u <= x and
A8: [x,y] in ab and
A9: y <= z ; :: thesis: [u,z] in ab
for Y being set st Y in X holds
[u,z] in Y
proof
let Y be set ; :: thesis: ( Y in X implies [u,z] in Y )
assume A10: Y in X ; :: thesis: [u,z] in Y
then A11: Y is auxiliary Relation of L by A1, Def8;
[x,y] in Y by A8, A10, SETFAM_1:def 1;
hence [u,z] in Y by A7, A9, A11, Def4; :: thesis: verum
end;
hence [u,z] in ab by SETFAM_1:def 1; :: thesis: verum
end;
A12: ab is auxiliary(iii)
proof
let x, y, z be Element of L; :: according to WAYBEL_4:def 5 :: thesis: ( [x,z] in ab & [y,z] in ab implies [(x "\/" y),z] in ab )
assume that
A13: [x,z] in ab and
A14: [y,z] in ab ; :: thesis: [(x "\/" y),z] in ab
for Y being set st Y in X holds
[(x "\/" y),z] in Y
proof
let Y be set ; :: thesis: ( Y in X implies [(x "\/" y),z] in Y )
assume A15: Y in X ; :: thesis: [(x "\/" y),z] in Y
then A16: Y is auxiliary Relation of L by A1, Def8;
A17: [x,z] in Y by A13, A15, SETFAM_1:def 1;
[y,z] in Y by A14, A15, SETFAM_1:def 1;
hence [(x "\/" y),z] in Y by A16, A17, Def5; :: thesis: verum
end;
hence [(x "\/" y),z] in ab by SETFAM_1:def 1; :: thesis: verum
end;
ab is auxiliary(iv)
proof
let x be Element of L; :: according to WAYBEL_4:def 6 :: thesis: [(Bottom L),x] in ab
for Y being set st Y in X holds
[(Bottom L),x] in Y
proof
let Y be set ; :: thesis: ( Y in X implies [(Bottom L),x] in Y )
assume Y in X ; :: thesis: [(Bottom L),x] in Y
then Y is auxiliary Relation of L by A1, Def8;
hence [(Bottom L),x] in Y by Def6; :: thesis: verum
end;
hence [(Bottom L),x] in ab by SETFAM_1:def 1; :: thesis: verum
end;
hence meet X is auxiliary Relation of L by A2, A6, A12; :: thesis: verum