set A = AuxBottom L;
A1: AuxBottom L is auxiliary(i)
proof
let x, y be Element of L; :: according to WAYBEL_4:def 3 :: thesis: ( [x,y] in AuxBottom L implies x <= y )
assume [x,y] in AuxBottom L ; :: thesis: x <= y
then x = Bottom L by Def9;
hence x <= y by YELLOW_0:44; :: thesis: verum
end;
A2: AuxBottom L 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 AuxBottom L & y <= z implies [u,z] in AuxBottom L )
assume that
A3: u <= x and
A4: [x,y] in AuxBottom L and
y <= z ; :: thesis: [u,z] in AuxBottom L
A5: x = Bottom L by A4, Def9;
Bottom L <= u by YELLOW_0:44;
then u = Bottom L by A3, A5, ORDERS_2:2;
hence [u,z] in AuxBottom L by Def9; :: thesis: verum
end;
A6: AuxBottom L is auxiliary(iii)
proof
let x, y, z be Element of L; :: according to WAYBEL_4:def 5 :: thesis: ( [x,z] in AuxBottom L & [y,z] in AuxBottom L implies [(x "\/" y),z] in AuxBottom L )
assume that
A7: [x,z] in AuxBottom L and
A8: [y,z] in AuxBottom L ; :: thesis: [(x "\/" y),z] in AuxBottom L
A9: y = Bottom L by A8, Def9;
then x <= y by A7, Def9;
then x "\/" y = Bottom L by A9, YELLOW_0:24;
hence [(x "\/" y),z] in AuxBottom L by Def9; :: thesis: verum
end;
for x being Element of L holds [(Bottom L),x] in AuxBottom L by Def9;
then AuxBottom L is auxiliary(iv) ;
hence AuxBottom L is auxiliary by A1, A2, A6; :: thesis: verum